Global Index

J

(1962 entries)

Notation Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

(121 entries)

Binder Index

J

W

_

(1392 entries)

Module Index

A

D

E

F

G

I

J

K

L

M

O

P

Q

R

T

U

V

W

X

Y

Z

_

other

(9 entries)

Variable Index

A

B

C

D

E

F

G

H

I

J

K

L

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(2 entries)

Library Index

F

J

K

P

Q

X

Y

Z

_

other

(60 entries)

Lemma Index

G

J

K

V

W

X

Y

other

(155 entries)

Constructor Index

A

D

E

F

G

H

I

J

K

O

P

Q

T

U

V

W

X

Y

Z

_

other

(27 entries)

Inductive Index

A

D

F

H

I

J

K

M

O

P

Q

R

T

U

V

W

X

Y

Z

_

other

(16 entries)

Projection Index

A

B

D

F

H

I

J

K

M

N

O

Q

R

S

U

V

X

Y

Z

_

other

(9 entries)

Section Index

A

B

E

F

G

H

I

J

K

L

N

O

P

Q

R

T

U

V

W

X

Y

Z

_

other

(6 entries)

Instance Index

A

C

D

F

H

I

J

K

M

N

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(56 entries)

Abbreviation Index

A

B

C

D

E

F

G

H

J

K

L

M

N

O

Q

R

S

T

U

V

W

X

Y

Z

_

other

(3 entries)

Definition Index

H

J

K

M

P

Q

R

U

V

W

X

Z

_

other

(100 entries)

Record Index

A

B

D

F

G

H

J

K

L

M

N

P

Q

R

T

U

V

W

X

Y

Z

_

other

(6 entries)

Global Index

A

acc_pt_bds_seq_ub [lemma, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
all_not_ex_func [lemma, in Waterproof.Libs.Negation]
all_func [lemma, in Waterproof.Libs.Negation]
alt_char_continuity [lemma, in Waterproof.Libs.Analysis.ContinuityDomainR]
alt_char_inf [lemma, in Waterproof.Libs.Analysis.SupAndInf]
alt_char_sup [lemma, in Waterproof.Libs.Analysis.SupAndInf]
alt_char_continuity [lemma, in Waterproof.Libs.Analysis.ContinuityDomainNat]
Analysis [library]
and_not_impl_func [lemma, in Waterproof.Libs.Negation]
and_not_or_func [lemma, in Waterproof.Libs.Negation]
and_func [lemma, in Waterproof.Libs.Negation]
any_low_bd_le_inf [lemma, in Waterproof.Libs.Analysis.SupAndInf]
any_upp_bd_ge_sup [lemma, in Waterproof.Libs.Analysis.SupAndInf]
archimed_mod [lemma, in Waterproof.Libs.Analysis.Sequences]
Assertions [library]
Assume [library]
Automation [library]
aux1 [lemma, in Waterproof.Libs.Analysis.ContinuityDomainNat]
a_seq [definition, in Waterproof.Libs.Analysis.Sequences]
a0:179 [binder, in Waterproof.Libs.Analysis.SupAndInf]
a0:18 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
a0:35 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
a0:50 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
A:1 [binder, in Waterproof.Tactics.Either]
a:1 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
A:1 [binder, in Waterproof.Util.Goals]
a:1 [binder, in Waterproof.Notations.Reals]
A:1 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
A:1 [binder, in Waterproof.Libs.Negation]
a:1 [binder, in Waterproof.Libs.Analysis.SequentialAccumulationPoints]
a:1 [binder, in Waterproof.Libs.Analysis.Subsequences]
a:1 [binder, in Waterproof.Libs.Analysis.Series]
a:1 [binder, in Waterproof.Libs.Analysis.ContinuityDomainR]
A:1 [binder, in Waterproof.Libs.Analysis.SupAndInf]
A:1 [binder, in Waterproof.Waterprove]
A:10 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
a:10 [binder, in Waterproof.Libs.Analysis.Sequences]
A:10 [binder, in Waterproof.Libs.Analysis.OpenAndClosed]
a:10 [binder, in Waterproof.Libs.Analysis.SupAndInf]
a:101 [binder, in Waterproof.Libs.Analysis.SupAndInf]
a:102 [binder, in Waterproof.Libs.Analysis.SupAndInf]
A:103 [binder, in Waterproof.Libs.Analysis.SupAndInf]
a:105 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
a:106 [binder, in Waterproof.Libs.Analysis.SupAndInf]
A:108 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
a:109 [binder, in Waterproof.Libs.Analysis.SupAndInf]
A:11 [binder, in Waterproof.Tactics.Either]
a:11 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
a:11 [binder, in Waterproof.Libs.Analysis.Series]
A:11 [binder, in Waterproof.Libs.Analysis.SupAndInf]
a:110 [binder, in Waterproof.Libs.Analysis.SupAndInf]
A:111 [binder, in Waterproof.Libs.Analysis.SupAndInf]
a:114 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
a:114 [binder, in Waterproof.Libs.Analysis.SupAndInf]
A:115 [binder, in Waterproof.Libs.Analysis.SupAndInf]
a:116 [binder, in Waterproof.Libs.Analysis.Sequences]
a:117 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
a:118 [binder, in Waterproof.Libs.Analysis.SupAndInf]
a:119 [binder, in Waterproof.Libs.Analysis.Sequences]
A:119 [binder, in Waterproof.Libs.Analysis.SupAndInf]
A:12 [binder, in Waterproof.Libs.Analysis.OpenAndClosed]
a:120 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
a:122 [binder, in Waterproof.Libs.Analysis.Sequences]
a:122 [binder, in Waterproof.Libs.Analysis.SupAndInf]
A:123 [binder, in Waterproof.Libs.Analysis.SupAndInf]
a:124 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
a:126 [binder, in Waterproof.Libs.Analysis.Sequences]
a:126 [binder, in Waterproof.Libs.Analysis.SupAndInf]
A:127 [binder, in Waterproof.Libs.Analysis.SupAndInf]
a:129 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
A:13 [binder, in Waterproof.Libs.Negation]
a:13 [binder, in Waterproof.Libs.Analysis.SubsequencesMetric]
a:13 [binder, in Waterproof.Libs.Analysis.SequencesMetric]
a:13 [binder, in Waterproof.Libs.Analysis.Series]
A:13 [binder, in Waterproof.Libs.Analysis.OpenAndClosed]
A:13 [binder, in Waterproof.Libs.Analysis.SupAndInf]
a:130 [binder, in Waterproof.Libs.Analysis.SupAndInf]
a:134 [binder, in Waterproof.Libs.Analysis.SupAndInf]
a:136 [binder, in Waterproof.Libs.Analysis.SupAndInf]
a:138 [binder, in Waterproof.Libs.Analysis.SupAndInf]
A:14 [binder, in Waterproof.Tactics.Either]
a:14 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
a:14 [binder, in Waterproof.Libs.Analysis.ContinuityDomainR]
a:14 [binder, in Waterproof.Libs.Analysis.ContinuityDomainNat]
A:140 [binder, in Waterproof.Chains.Inequalities]
a:142 [binder, in Waterproof.Libs.Analysis.SupAndInf]
A:143 [binder, in Waterproof.Libs.Analysis.SupAndInf]
A:146 [binder, in Waterproof.Chains.Inequalities]
a:146 [binder, in Waterproof.Libs.Analysis.SupAndInf]
A:15 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
a:15 [binder, in Waterproof.Libs.Analysis.Series]
A:15 [binder, in Waterproof.Libs.Analysis.OpenAndClosed]
a:15 [binder, in Waterproof.Libs.Analysis.ContinuityDomainR]
a:150 [binder, in Waterproof.Libs.Analysis.SupAndInf]
A:152 [binder, in Waterproof.Chains.Inequalities]
a:152 [binder, in Waterproof.Libs.Analysis.SupAndInf]
a:154 [binder, in Waterproof.Libs.Analysis.SupAndInf]
a:156 [binder, in Waterproof.Libs.Analysis.SupAndInf]
A:158 [binder, in Waterproof.Chains.Inequalities]
A:16 [binder, in Waterproof.Chains.Inequalities]
A:16 [binder, in Waterproof.Libs.Analysis.SupAndInf]
A:160 [binder, in Waterproof.Libs.Analysis.SupAndInf]
a:162 [binder, in Waterproof.Libs.Analysis.SupAndInf]
a:163 [binder, in Waterproof.Libs.Analysis.SupAndInf]
a:164 [binder, in Waterproof.Libs.Analysis.SupAndInf]
a:165 [binder, in Waterproof.Libs.Analysis.SupAndInf]
a:166 [binder, in Waterproof.Libs.Analysis.SupAndInf]
A:167 [binder, in Waterproof.Libs.Analysis.SupAndInf]
A:17 [binder, in Waterproof.Tactics.Either]
a:17 [binder, in Waterproof.Libs.Analysis.ContinuityDomainNat]
A:170 [binder, in Waterproof.Libs.Analysis.SupAndInf]
a:173 [binder, in Waterproof.Libs.Analysis.SupAndInf]
a:18 [binder, in Waterproof.Libs.Analysis.Series]
a:18 [binder, in Waterproof.Libs.Reals]
A:18 [binder, in Waterproof.Libs.Analysis.SupAndInf]
a:182 [binder, in Waterproof.Libs.Analysis.SupAndInf]
a:186 [binder, in Waterproof.Libs.Analysis.SupAndInf]
A:19 [binder, in Waterproof.Libs.Negation]
a:19 [binder, in Waterproof.Libs.Analysis.ContinuityDomainR]
a:2 [binder, in Waterproof.Libs.Analysis.SequencesMetric]
A:20 [binder, in Waterproof.Tactics.Either]
a:20 [binder, in Waterproof.Libs.Analysis.Sequences]
a:20 [binder, in Waterproof.Libs.Reals]
a:21 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
A:21 [binder, in Waterproof.Libs.Analysis.SupAndInf]
a:21 [binder, in Waterproof.Libs.Analysis.ContinuityDomainNat]
a:22 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
A:23 [binder, in Waterproof.Tactics.Either]
A:24 [binder, in Waterproof.Libs.Analysis.SupAndInf]
A:25 [binder, in Waterproof.Libs.Negation]
a:26 [binder, in Waterproof.Libs.Analysis.SupAndInf]
A:27 [binder, in Waterproof.Util.Goals]
a:27 [binder, in Waterproof.Libs.Analysis.ContinuityDomainNat]
A:28 [binder, in Waterproof.Chains.Inequalities]
A:28 [binder, in Waterproof.Libs.Analysis.SupAndInf]
a:29 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
A:29 [binder, in Waterproof.Libs.Negation]
a:29 [binder, in Waterproof.Libs.Analysis.ContinuityDomainNat]
A:3 [binder, in Waterproof.Tactics.Either]
A:3 [binder, in Waterproof.Libs.Analysis.SupAndInf]
a:30 [binder, in Waterproof.Libs.Reals]
a:30 [binder, in Waterproof.Libs.Analysis.SupAndInf]
A:31 [binder, in Waterproof.Libs.Analysis.SupAndInf]
A:32 [binder, in Waterproof.Util.Goals]
A:32 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
a:32 [binder, in Waterproof.Libs.Analysis.Subsequences]
a:32 [binder, in Waterproof.Libs.Analysis.SubsequencesMetric]
a:32 [binder, in Waterproof.Libs.Reals]
A:33 [binder, in Waterproof.Libs.Negation]
A:34 [binder, in Waterproof.Libs.Analysis.SupAndInf]
A:37 [binder, in Waterproof.Util.Goals]
A:37 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
A:37 [binder, in Waterproof.Libs.Negation]
a:39 [binder, in Waterproof.Libs.Analysis.SupAndInf]
a:4 [binder, in Waterproof.Libs.Analysis.OpenAndClosed]
a:4 [binder, in Waterproof.Libs.Analysis.ContinuityDomainR]
a:4 [binder, in Waterproof.Libs.Analysis.SupAndInf]
a:40 [binder, in Waterproof.Libs.Analysis.Subsequences]
A:41 [binder, in Waterproof.Util.Goals]
A:41 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
A:41 [binder, in Waterproof.Libs.Negation]
A:44 [binder, in Waterproof.Libs.Negation]
a:44 [binder, in Waterproof.Libs.Analysis.Sequences]
A:44 [binder, in Waterproof.Libs.Analysis.SupAndInf]
A:47 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
A:47 [binder, in Waterproof.Libs.Negation]
a:49 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
A:5 [binder, in Waterproof.Util.Goals]
A:5 [binder, in Waterproof.Libs.Negation]
a:5 [binder, in Waterproof.Libs.Analysis.SequentialAccumulationPoints]
a:5 [binder, in Waterproof.Libs.Analysis.Series]
A:5 [binder, in Waterproof.Libs.Analysis.OpenAndClosed]
A:50 [binder, in Waterproof.Libs.Negation]
A:50 [binder, in Waterproof.Libs.Analysis.SupAndInf]
A:53 [binder, in Waterproof.Libs.Negation]
A:54 [binder, in Waterproof.Libs.Analysis.SupAndInf]
a:55 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
a:57 [binder, in Waterproof.Libs.Analysis.Sequences]
A:58 [binder, in Waterproof.Libs.Analysis.SupAndInf]
A:59 [binder, in Waterproof.Libs.Negation]
a:6 [binder, in Waterproof.Libs.Analysis.Sequences]
A:61 [binder, in Waterproof.Libs.Analysis.SupAndInf]
A:65 [binder, in Waterproof.Libs.Negation]
A:65 [binder, in Waterproof.Libs.Analysis.SupAndInf]
a:67 [binder, in Waterproof.Libs.Analysis.Sequences]
a:68 [binder, in Waterproof.Libs.Analysis.SupAndInf]
a:69 [binder, in Waterproof.Libs.Analysis.SupAndInf]
A:7 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
a:71 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
A:71 [binder, in Waterproof.Libs.Negation]
A:71 [binder, in Waterproof.Libs.Analysis.SupAndInf]
a:74 [binder, in Waterproof.Libs.Analysis.Sequences]
a:74 [binder, in Waterproof.Libs.Analysis.SupAndInf]
a:75 [binder, in Waterproof.Libs.Analysis.SupAndInf]
A:77 [binder, in Waterproof.Libs.Negation]
A:77 [binder, in Waterproof.Libs.Analysis.SupAndInf]
A:79 [binder, in Waterproof.Libs.Negation]
A:8 [binder, in Waterproof.Tactics.Either]
a:8 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
a:8 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
a:8 [binder, in Waterproof.Libs.Analysis.SequencesMetric]
A:8 [binder, in Waterproof.Libs.Analysis.OpenAndClosed]
a:8 [binder, in Waterproof.Libs.Analysis.ContinuityDomainR]
A:8 [binder, in Waterproof.Libs.Analysis.SupAndInf]
a:80 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
a:80 [binder, in Waterproof.Libs.Analysis.SupAndInf]
a:83 [binder, in Waterproof.Libs.Analysis.SupAndInf]
a:84 [binder, in Waterproof.Libs.Analysis.SupAndInf]
a:85 [binder, in Waterproof.Libs.Analysis.SupAndInf]
A:86 [binder, in Waterproof.Libs.Analysis.SupAndInf]
a:89 [binder, in Waterproof.Libs.Analysis.SupAndInf]
A:9 [binder, in Waterproof.Libs.Negation]
a:9 [binder, in Waterproof.Libs.Analysis.SubsequencesMetric]
a:9 [binder, in Waterproof.Libs.Analysis.Series]
a:9 [binder, in Waterproof.Libs.Analysis.OpenAndClosed]
a:90 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
a:90 [binder, in Waterproof.Libs.Analysis.Sequences]
a:92 [binder, in Waterproof.Libs.Analysis.Subsequences]
a:92 [binder, in Waterproof.Libs.Analysis.SupAndInf]
a:93 [binder, in Waterproof.Libs.Analysis.SupAndInf]
a:94 [binder, in Waterproof.Libs.Analysis.Sequences]
a:94 [binder, in Waterproof.Libs.Analysis.SupAndInf]
A:95 [binder, in Waterproof.Libs.Analysis.SupAndInf]
a:97 [binder, in Waterproof.Libs.Analysis.Sequences]
a:98 [binder, in Waterproof.Libs.Analysis.SupAndInf]

B

base_gc_R_Z [instance, in Waterproof.Chains.Inequalities]
base_gc_Z_R [instance, in Waterproof.Chains.Inequalities]
base_lc_R_Z [instance, in Waterproof.Chains.Inequalities]
base_lc_Z_R [instance, in Waterproof.Chains.Inequalities]
base_ec_R_Z [instance, in Waterproof.Chains.Inequalities]
base_ec_Z_R [instance, in Waterproof.Chains.Inequalities]
base_gc_R_nat [instance, in Waterproof.Chains.Inequalities]
base_gc_nat_R [instance, in Waterproof.Chains.Inequalities]
base_lc_R_nat [instance, in Waterproof.Chains.Inequalities]
base_lc_nat_R [instance, in Waterproof.Chains.Inequalities]
base_ec_R_nat [instance, in Waterproof.Chains.Inequalities]
base_ec_nat_R [instance, in Waterproof.Chains.Inequalities]
base_gc_inst [instance, in Waterproof.Chains.Inequalities]
base_lc_inst [instance, in Waterproof.Chains.Inequalities]
base_ec_inst [instance, in Waterproof.Chains.Inequalities]
base_gc [constructor, in Waterproof.Chains.Inequalities]
base_lc [constructor, in Waterproof.Chains.Inequalities]
base_ec [constructor, in Waterproof.Chains.Inequalities]
bdd_below_to_bdd_above_set_opp [lemma, in Waterproof.Libs.Analysis.SupAndInf]
Because [library]
Binders [library]
Bolzano_Weierstrass [lemma, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
Bolzano_Weierstrass_gen [lemma, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
BothDirections [library]
BothStatements [library]
bounded [definition, in Waterproof.Libs.Analysis.SequencesMetric]
bounded_by_lower_bound_propform [lemma, in Waterproof.Libs.Analysis.SupAndInf]
bounded_by_upper_bound_propform [lemma, in Waterproof.Libs.Analysis.SupAndInf]
build_seq [definition, in Waterproof.Libs.Analysis.Subsequences]
built_seq_is_index_seq [lemma, in Waterproof.Libs.Analysis.Subsequences]
ByContradiction [module, in Waterproof.Util.Goals]
ByContradiction.unwrap [definition, in Waterproof.Util.Goals]
ByContradiction.wrap [constructor, in Waterproof.Util.Goals]
ByContradiction.Wrapper [inductive, in Waterproof.Util.Goals]
B:10 [binder, in Waterproof.Libs.Negation]
B:109 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
b:11 [binder, in Waterproof.Libs.Analysis.Sequences]
b:115 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
b:118 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
B:12 [binder, in Waterproof.Tactics.Either]
b:121 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
b:126 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
b:131 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
b:134 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
b:138 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
B:141 [binder, in Waterproof.Chains.Inequalities]
B:147 [binder, in Waterproof.Chains.Inequalities]
B:15 [binder, in Waterproof.Tactics.Either]
B:153 [binder, in Waterproof.Chains.Inequalities]
B:159 [binder, in Waterproof.Chains.Inequalities]
b:169 [binder, in Waterproof.Libs.Analysis.SupAndInf]
B:17 [binder, in Waterproof.Chains.Inequalities]
b:172 [binder, in Waterproof.Libs.Analysis.SupAndInf]
B:18 [binder, in Waterproof.Tactics.Either]
b:19 [binder, in Waterproof.Libs.Reals]
B:2 [binder, in Waterproof.Tactics.Either]
B:2 [binder, in Waterproof.Libs.Negation]
B:2 [binder, in Waterproof.Waterprove]
b:20 [binder, in Waterproof.Libs.Analysis.SupAndInf]
B:21 [binder, in Waterproof.Tactics.Either]
b:21 [binder, in Waterproof.Libs.Analysis.Sequences]
b:21 [binder, in Waterproof.Libs.Reals]
b:23 [binder, in Waterproof.Libs.Analysis.SupAndInf]
B:24 [binder, in Waterproof.Tactics.Either]
B:26 [binder, in Waterproof.Libs.Negation]
b:27 [binder, in Waterproof.Libs.Analysis.SupAndInf]
B:29 [binder, in Waterproof.Chains.Inequalities]
B:30 [binder, in Waterproof.Libs.Negation]
b:31 [binder, in Waterproof.Libs.Reals]
b:33 [binder, in Waterproof.Libs.Reals]
B:34 [binder, in Waterproof.Libs.Negation]
B:38 [binder, in Waterproof.Libs.Negation]
b:39 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
B:4 [binder, in Waterproof.Tactics.Either]
b:4 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
b:42 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
B:42 [binder, in Waterproof.Libs.Negation]
b:43 [binder, in Waterproof.Libs.Analysis.SupAndInf]
B:45 [binder, in Waterproof.Libs.Negation]
b:45 [binder, in Waterproof.Libs.Analysis.Sequences]
B:48 [binder, in Waterproof.Libs.Negation]
B:51 [binder, in Waterproof.Libs.Negation]
b:52 [binder, in Waterproof.Libs.Analysis.SupAndInf]
B:6 [binder, in Waterproof.Libs.Negation]
b:7 [binder, in Waterproof.Libs.Analysis.Sequences]
b:75 [binder, in Waterproof.Libs.Analysis.Sequences]
B:78 [binder, in Waterproof.Libs.Negation]
b:8 [binder, in Waterproof.Libs.Analysis.SubsequencesMetric]
B:80 [binder, in Waterproof.Libs.Negation]
B:9 [binder, in Waterproof.Tactics.Either]
b:93 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
b:96 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]

C

Case [module, in Waterproof.Util.Goals]
Case.unwrap [definition, in Waterproof.Util.Goals]
Case.wrap [constructor, in Waterproof.Util.Goals]
Case.Wrapper [inductive, in Waterproof.Util.Goals]
ChainBase [record, in Waterproof.Chains.Inequalities]
ChainBase [inductive, in Waterproof.Chains.Inequalities]
ChainLink [record, in Waterproof.Chains.Inequalities]
ChainLink [inductive, in Waterproof.Chains.Inequalities]
Chains [library]
chain_base [projection, in Waterproof.Chains.Inequalities]
chain_base [constructor, in Waterproof.Chains.Inequalities]
chain_link [projection, in Waterproof.Chains.Inequalities]
chain_link [constructor, in Waterproof.Chains.Inequalities]
chain_ge [constructor, in Waterproof.Chains.Inequalities]
chain_gt [constructor, in Waterproof.Chains.Inequalities]
chain_le [constructor, in Waterproof.Chains.Inequalities]
chain_lt [constructor, in Waterproof.Chains.Inequalities]
chain_eq [constructor, in Waterproof.Chains.Inequalities]
Choose [library]
Claims [library]
classic_strong_ind_index_seq_with_prop [lemma, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
Common [library]
complement [definition, in Waterproof.Libs.Analysis.OpenAndClosed]
Conclusion [library]
constant_sequence [definition, in Waterproof.Libs.Analysis.Sequences]
Constr [library]
Construction [section, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
ConstructiveLogic [library]
const_seq_from [definition, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
const_seq [definition, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
ContinuityDomainNat [library]
ContinuityDomainR [library]
Contradiction [library]
convergence [definition, in Waterproof.Libs.Analysis.SequencesMetric]
convergence_equivalence [lemma, in Waterproof.Libs.Analysis.Sequences]
converges_to [definition, in Waterproof.Notations.Reals]
conv_evt_eq_seq [lemma, in Waterproof.Libs.Analysis.Sequences]
created_seq_is_index_seq [lemma, in Waterproof.Libs.Analysis.Subsequences]
create_seq [definition, in Waterproof.Libs.Analysis.Subsequences]
cv_implies_cv_abs_to_l_abs [definition, in Waterproof.Notations.Reals]
C:10 [binder, in Waterproof.Tactics.Either]
c:100 [binder, in Waterproof.Chains.Inequalities]
c:103 [binder, in Waterproof.Chains.Inequalities]
c:106 [binder, in Waterproof.Chains.Inequalities]
C:11 [binder, in Waterproof.Libs.Negation]
C:110 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
c:113 [binder, in Waterproof.Chains.Inequalities]
c:116 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
c:116 [binder, in Waterproof.Chains.Inequalities]
c:119 [binder, in Waterproof.Chains.Inequalities]
C:13 [binder, in Waterproof.Tactics.Either]
c:143 [binder, in Waterproof.Chains.Inequalities]
c:149 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
c:149 [binder, in Waterproof.Chains.Inequalities]
c:151 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
c:155 [binder, in Waterproof.Chains.Inequalities]
C:16 [binder, in Waterproof.Tactics.Either]
C:160 [binder, in Waterproof.Chains.Inequalities]
C:18 [binder, in Waterproof.Chains.Inequalities]
C:19 [binder, in Waterproof.Tactics.Either]
c:2 [binder, in Waterproof.Notations.Reals]
C:22 [binder, in Waterproof.Tactics.Either]
C:25 [binder, in Waterproof.Tactics.Either]
C:27 [binder, in Waterproof.Libs.Negation]
c:27 [binder, in Waterproof.Libs.Analysis.Sequences]
c:29 [binder, in Waterproof.Libs.Analysis.Sequences]
C:3 [binder, in Waterproof.Libs.Negation]
c:3 [binder, in Waterproof.Libs.Analysis.SequencesMetric]
C:3 [binder, in Waterproof.Waterprove]
C:30 [binder, in Waterproof.Chains.Inequalities]
C:31 [binder, in Waterproof.Libs.Negation]
C:35 [binder, in Waterproof.Libs.Negation]
c:37 [binder, in Waterproof.Chains.Inequalities]
C:39 [binder, in Waterproof.Libs.Negation]
c:41 [binder, in Waterproof.Chains.Inequalities]
C:43 [binder, in Waterproof.Libs.Negation]
c:45 [binder, in Waterproof.Chains.Inequalities]
C:46 [binder, in Waterproof.Libs.Negation]
c:46 [binder, in Waterproof.Libs.Analysis.Sequences]
C:49 [binder, in Waterproof.Libs.Negation]
c:49 [binder, in Waterproof.Chains.Inequalities]
C:5 [binder, in Waterproof.Tactics.Either]
c:5 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
C:52 [binder, in Waterproof.Libs.Negation]
c:52 [binder, in Waterproof.Chains.Inequalities]
c:55 [binder, in Waterproof.Chains.Inequalities]
C:58 [binder, in Waterproof.Chains.Inequalities]
C:7 [binder, in Waterproof.Libs.Negation]
c:72 [binder, in Waterproof.Chains.Inequalities]
c:75 [binder, in Waterproof.Chains.Inequalities]
c:87 [binder, in Waterproof.Chains.Inequalities]
c:91 [binder, in Waterproof.Chains.Inequalities]

D

d [definition, in Waterproof.Libs.Analysis.Sequences]
Define [library]
Definitions [section, in Waterproof.Libs.Analysis.MetricSpaces]
dep_choice [definition, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
dep_only_on_start_index_seq_prop_family [lemma, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
dep_only_on_start [definition, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
dist_reflexive [definition, in Waterproof.Libs.Analysis.MetricSpaces]
dist_triangle_inequality [definition, in Waterproof.Libs.Analysis.MetricSpaces]
dist_symmetric [definition, in Waterproof.Libs.Analysis.MetricSpaces]
dist_non_degenerate [definition, in Waterproof.Libs.Analysis.MetricSpaces]
dist_positive [definition, in Waterproof.Libs.Analysis.MetricSpaces]
diverges_to_minus_infinity [definition, in Waterproof.Libs.Analysis.Sequences]
diverges_to_plus_infinity [definition, in Waterproof.Libs.Analysis.Sequences]
div_pos [lemma, in Waterproof.Libs.Reals]
div_sign_flip [lemma, in Waterproof.Libs.Reals]
double_sumbool_sumtriad_cba [lemma, in Waterproof.Tactics.Either]
double_sumbool_sumtriad_cab [lemma, in Waterproof.Tactics.Either]
double_sumbool_sumtriad_bca [lemma, in Waterproof.Tactics.Either]
double_sumbool_sumtriad_bac [lemma, in Waterproof.Tactics.Either]
double_sumbool_sumtriad_acb [lemma, in Waterproof.Tactics.Either]
double_sumbool_sumtriad_abc [lemma, in Waterproof.Tactics.Either]
double_is_even [lemma, in Waterproof.Libs.Analysis.SubsequencesMetric]
d_discrete_R [definition, in Waterproof.Libs.Analysis.MetricSpaces]
d'_eq_3 [lemma, in Waterproof.Libs.Analysis.MetricSpaces]
d'_eq_0 [lemma, in Waterproof.Libs.Analysis.MetricSpaces]
D:111 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
D:12 [binder, in Waterproof.Libs.Negation]
d:122 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
d:127 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
d:132 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
d:136 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
d:140 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
d:142 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
d:145 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
D:28 [binder, in Waterproof.Libs.Negation]
D:32 [binder, in Waterproof.Libs.Negation]
D:36 [binder, in Waterproof.Libs.Negation]
D:4 [binder, in Waterproof.Libs.Negation]
D:40 [binder, in Waterproof.Libs.Negation]
D:8 [binder, in Waterproof.Libs.Negation]

E

ecn:167 [binder, in Waterproof.Chains.Inequalities]
ecn:175 [binder, in Waterproof.Chains.Inequalities]
ecn:191 [binder, in Waterproof.Chains.Inequalities]
ecn:207 [binder, in Waterproof.Chains.Inequalities]
ecn:215 [binder, in Waterproof.Chains.Inequalities]
ecn:231 [binder, in Waterproof.Chains.Inequalities]
ecx:169 [binder, in Waterproof.Chains.Inequalities]
ecx:177 [binder, in Waterproof.Chains.Inequalities]
ecx:193 [binder, in Waterproof.Chains.Inequalities]
ecx:209 [binder, in Waterproof.Chains.Inequalities]
ecx:217 [binder, in Waterproof.Chains.Inequalities]
ecx:233 [binder, in Waterproof.Chains.Inequalities]
ec_map [definition, in Waterproof.Chains.Inequalities]
ec_interpretable [instance, in Waterproof.Chains.Inequalities]
ec_total_statement [definition, in Waterproof.Chains.Inequalities]
ec_global_statement [definition, in Waterproof.Chains.Inequalities]
ec_tail [definition, in Waterproof.Chains.Inequalities]
ec_head [definition, in Waterproof.Chains.Inequalities]
Either [library]
elements_le_seq_of_max [lemma, in Waterproof.Libs.Analysis.Subsequences]
elements_le_seq_of_max_pre [lemma, in Waterproof.Libs.Analysis.Subsequences]
empty [definition, in Waterproof.Notations.Sets]
eps:62 [binder, in Waterproof.Libs.Analysis.Sequences]
eps:80 [binder, in Waterproof.Libs.Analysis.Sequences]
eps:83 [binder, in Waterproof.Libs.Analysis.Sequences]
EqualChain [inductive, in Waterproof.Chains.Inequalities]
EqualInterpretation [record, in Waterproof.Chains.Inequalities]
EqualInterpretation0:71 [binder, in Waterproof.Chains.Inequalities]
EqualInterpretation0:74 [binder, in Waterproof.Chains.Inequalities]
EqualInterpretation0:79 [binder, in Waterproof.Chains.Inequalities]
EqualRel [inductive, in Waterproof.Chains.Inequalities]
equal_interpretation [instance, in Waterproof.Chains.Inequalities]
equivalent_subsequence_convergence [lemma, in Waterproof.Libs.Analysis.SubsequencesMetric]
eq_seq_conv_to_same_lim [lemma, in Waterproof.Libs.Analysis.Sequences]
eq_rel_to_pred [projection, in Waterproof.Chains.Inequalities]
Evars [library]
every_point_in_R_acc_point_R [lemma, in Waterproof.Libs.Analysis.ContinuityDomainR]
evt_eq_sequences [definition, in Waterproof.Libs.Analysis.Sequences]
existence_next_el_to_fun [lemma, in Waterproof.Libs.Analysis.Subsequences]
exists_subseq_to_limsup_bdd [lemma, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
exists_almost_lim_sup [lemma, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
exists_good_subseq [lemma, in Waterproof.Libs.Analysis.Subsequences]
exists_almost_lim_sup_aux [lemma, in Waterproof.Libs.Analysis.SupAndInf]
exists_almost_minimizer_ε [lemma, in Waterproof.Libs.Analysis.SupAndInf]
exists_almost_maximizer_ε [lemma, in Waterproof.Libs.Analysis.SupAndInf]
exists_almost_minimizer [lemma, in Waterproof.Libs.Analysis.SupAndInf]
exists_almost_maximizer [lemma, in Waterproof.Libs.Analysis.SupAndInf]
exists_inf [lemma, in Waterproof.Libs.Analysis.SupAndInf]
ex_not_all_func [lemma, in Waterproof.Libs.Negation]
ex_func [lemma, in Waterproof.Libs.Negation]
E:112 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
e:123 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
e:128 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
e:133 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
e:137 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
e:141 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
e:144 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
e:147 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
e:148 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
e:150 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]

F

false_Req [lemma, in Waterproof.Libs.Reals]
finite_or_find_one [lemma, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
finite_triangle_inequalty [definition, in Waterproof.Notations.Reals]
first_satisfying_element [definition, in Waterproof.Libs.Analysis.Subsequences]
first_satisfying_element_helper [definition, in Waterproof.Libs.Analysis.Subsequences]
full [definition, in Waterproof.Notations.Sets]
f:100 [binder, in Waterproof.Libs.Analysis.Subsequences]
f:108 [binder, in Waterproof.Libs.Analysis.Subsequences]
f:115 [binder, in Waterproof.Libs.Analysis.Subsequences]
f:119 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
f:125 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
f:13 [binder, in Waterproof.Libs.Analysis.ContinuityDomainR]
f:130 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
f:135 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
f:139 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
f:142 [binder, in Waterproof.Chains.Inequalities]
f:143 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
f:146 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
f:148 [binder, in Waterproof.Chains.Inequalities]
f:154 [binder, in Waterproof.Chains.Inequalities]
f:161 [binder, in Waterproof.Chains.Inequalities]
f:20 [binder, in Waterproof.Libs.Analysis.ContinuityDomainNat]
f:22 [binder, in Waterproof.Libs.Analysis.Subsequences]
f:26 [binder, in Waterproof.Libs.Analysis.ContinuityDomainNat]
f:6 [binder, in Waterproof.Libs.Analysis.Subsequences]
f:62 [binder, in Waterproof.Libs.Analysis.Subsequences]
f:7 [binder, in Waterproof.Libs.Analysis.ContinuityDomainR]
f:96 [binder, in Waterproof.Libs.Analysis.Subsequences]

G

gcn:195 [binder, in Waterproof.Chains.Inequalities]
gcn:199 [binder, in Waterproof.Chains.Inequalities]
gcn:235 [binder, in Waterproof.Chains.Inequalities]
gcn:239 [binder, in Waterproof.Chains.Inequalities]
gcx:197 [binder, in Waterproof.Chains.Inequalities]
gcx:201 [binder, in Waterproof.Chains.Inequalities]
gcx:237 [binder, in Waterproof.Chains.Inequalities]
gcx:241 [binder, in Waterproof.Chains.Inequalities]
gc_map [definition, in Waterproof.Chains.Inequalities]
gc_interpretable [instance, in Waterproof.Chains.Inequalities]
gc_total_statement [definition, in Waterproof.Chains.Inequalities]
gc_weak_global_statement [definition, in Waterproof.Chains.Inequalities]
gc_global_statement [definition, in Waterproof.Chains.Inequalities]
gc_tail [definition, in Waterproof.Chains.Inequalities]
gc_head [definition, in Waterproof.Chains.Inequalities]
global_grtr_rel [definition, in Waterproof.Chains.Inequalities]
global_less_rel [definition, in Waterproof.Chains.Inequalities]
global_statement [projection, in Waterproof.Chains.Inequalities]
Goals [library]
GreaterChain [inductive, in Waterproof.Chains.Inequalities]
GreaterRel [inductive, in Waterproof.Chains.Inequalities]
grtr_rel_to_pred [projection, in Waterproof.Chains.Inequalities]
grtr_relation_flow [definition, in Waterproof.Chains.Inequalities]
g:104 [binder, in Waterproof.Libs.Analysis.Subsequences]
g:106 [binder, in Waterproof.Libs.Analysis.Subsequences]
g:112 [binder, in Waterproof.Libs.Analysis.Subsequences]
g:119 [binder, in Waterproof.Libs.Analysis.Subsequences]
G:12 [binder, in Waterproof.Util.Goals]
g:13 [binder, in Waterproof.Libs.Analysis.Subsequences]
G:15 [binder, in Waterproof.Util.Goals]
G:18 [binder, in Waterproof.Util.Goals]
g:18 [binder, in Waterproof.Libs.Analysis.SubsequencesMetric]
G:2 [binder, in Waterproof.Util.Goals]
g:20 [binder, in Waterproof.Libs.Analysis.SubsequencesMetric]
G:21 [binder, in Waterproof.Util.Goals]
G:24 [binder, in Waterproof.Util.Goals]
g:26 [binder, in Waterproof.Libs.Analysis.Subsequences]
G:29 [binder, in Waterproof.Util.Goals]
g:33 [binder, in Waterproof.Libs.Analysis.Subsequences]
G:34 [binder, in Waterproof.Util.Goals]
G:38 [binder, in Waterproof.Util.Goals]
G:42 [binder, in Waterproof.Util.Goals]
G:45 [binder, in Waterproof.Util.Goals]
G:48 [binder, in Waterproof.Util.Goals]
g:50 [binder, in Waterproof.Libs.Analysis.Subsequences]
G:6 [binder, in Waterproof.Util.Goals]
g:64 [binder, in Waterproof.Libs.Analysis.Subsequences]
G:9 [binder, in Waterproof.Util.Goals]

H

Help [library]
HelpNewHyp [module, in Waterproof.Tactics.Help]
help_with_choice [lemma, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
Hints [library]
Hstep:101 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
Hstep:160 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
Hstep:23 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
Hstep:57 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
Hypothesis [library]
HypP:17 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
HypP:49 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
H0:154 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
H0:19 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
H0:51 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
H0:95 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
h:18 [binder, in Waterproof.Libs.Analysis.Subsequences]
h:18 [binder, in Waterproof.Libs.Analysis.ContinuityDomainR]
h:28 [binder, in Waterproof.Util.Goals]
h:28 [binder, in Waterproof.Libs.Analysis.ContinuityDomainNat]
h:33 [binder, in Waterproof.Util.Goals]

I

if_almost_minimizer_ε_then_every_low_bd_smaller [lemma, in Waterproof.Libs.Analysis.SupAndInf]
if_almost_maximizer_ε_then_every_upp_bd_larger [lemma, in Waterproof.Libs.Analysis.SupAndInf]
if_almost_minimizer_then_every_low_bd_smaller [lemma, in Waterproof.Libs.Analysis.SupAndInf]
if_almost_maximizer_then_every_upp_bd_larger [lemma, in Waterproof.Libs.Analysis.SupAndInf]
ii:10 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
ii:16 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
ii:23 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
ii:51 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
ii:92 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
impl_not_and_func [lemma, in Waterproof.Libs.Negation]
impl_func [lemma, in Waterproof.Libs.Negation]
incr_loc_to_glob [lemma, in Waterproof.Libs.Analysis.Subsequences]
incr_loc_to_glob [lemma, in Waterproof.Libs.Analysis.SubsequencesMetric]
index_seq_prop_family [definition, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
index_seq_grows [lemma, in Waterproof.Libs.Analysis.Subsequences]
index_seq_grows_0 [lemma, in Waterproof.Libs.Analysis.Subsequences]
index_seq_strictly_incr [lemma, in Waterproof.Libs.Analysis.Subsequences]
index_sequence_property2 [lemma, in Waterproof.Libs.Analysis.SubsequencesMetric]
index_seq_equiv [lemma, in Waterproof.Libs.Analysis.SubsequencesMetric]
index_sequence_property [lemma, in Waterproof.Libs.Analysis.SubsequencesMetric]
Induction [library]
ind_seq_with_prop [definition, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
ind_seq_of_seq_and_prop [definition, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
Inequalities [library]
InformativeEpsilon [library]
informative_or_lift [lemma, in Waterproof.Libs.Logic.InformativeEpsilon]
inf_el_to_fun [lemma, in Waterproof.Libs.Analysis.Subsequences]
inf_is_low_bd [lemma, in Waterproof.Libs.Analysis.SupAndInf]
Init [library]
InterpretableChain [record, in Waterproof.Chains.Inequalities]
inv_remove [lemma, in Waterproof.Libs.Reals]
in_implies_not_in_compl [lemma, in Waterproof.Libs.Analysis.OpenAndClosed]
is_seq_acc_pt [definition, in Waterproof.Libs.Analysis.SequentialAccumulationPoints]
is_increasing [definition, in Waterproof.Libs.Analysis.Subsequences]
is_index_seq [definition, in Waterproof.Libs.Analysis.Subsequences]
is_increasing [definition, in Waterproof.Libs.Analysis.SubsequencesMetric]
is_accumulation_point [definition, in Waterproof.Libs.Analysis.SubsequencesMetric]
is_subsequence [definition, in Waterproof.Libs.Analysis.SubsequencesMetric]
is_index_seq [definition, in Waterproof.Libs.Analysis.SubsequencesMetric]
is_index_sequence [definition, in Waterproof.Libs.Analysis.SubsequencesMetric]
is_bounded_below [definition, in Waterproof.Libs.Analysis.Sequences]
is_bounded_above [definition, in Waterproof.Libs.Analysis.Sequences]
is_bounded_equivalence [lemma, in Waterproof.Libs.Analysis.Sequences]
is_bounded_equivalent [definition, in Waterproof.Libs.Analysis.Sequences]
is_bounded [definition, in Waterproof.Libs.Analysis.Sequences]
is_closed [definition, in Waterproof.Libs.Analysis.OpenAndClosed]
is_open [definition, in Waterproof.Libs.Analysis.OpenAndClosed]
is_interior_point [definition, in Waterproof.Libs.Analysis.OpenAndClosed]
is_continuous_in [definition, in Waterproof.Libs.Analysis.ContinuityDomainR]
is_isolated_point [definition, in Waterproof.Libs.Analysis.ContinuityDomainR]
is_accumulation_point [definition, in Waterproof.Libs.Analysis.ContinuityDomainR]
is_inf_alt_char [definition, in Waterproof.Libs.Analysis.SupAndInf]
is_sup_alt_char [definition, in Waterproof.Libs.Analysis.SupAndInf]
is_inf [definition, in Waterproof.Libs.Analysis.SupAndInf]
is_bounded_below [definition, in Waterproof.Libs.Analysis.SupAndInf]
is_lower_bound [definition, in Waterproof.Libs.Analysis.SupAndInf]
is_max [definition, in Waterproof.Libs.Analysis.SupAndInf]
is_sup [abbreviation, in Waterproof.Libs.Analysis.SupAndInf]
is_bounded_above [abbreviation, in Waterproof.Libs.Analysis.SupAndInf]
is_continuous_in [definition, in Waterproof.Libs.Analysis.ContinuityDomainNat]
is_isolated_point [definition, in Waterproof.Libs.Analysis.ContinuityDomainNat]
is_accumulation_point [definition, in Waterproof.Libs.Analysis.ContinuityDomainNat]
ItHolds [library]
ItSuffices [library]
i:15 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
i:22 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
i:30 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
i:50 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
i:81 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
i:9 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
i:91 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]

K

k0:20 [binder, in Waterproof.Libs.Analysis.SequentialAccumulationPoints]
k0:74 [binder, in Waterproof.Libs.Analysis.Subsequences]
k0:77 [binder, in Waterproof.Libs.Analysis.Subsequences]
k1:28 [binder, in Waterproof.Libs.Analysis.SubsequencesMetric]
k2:29 [binder, in Waterproof.Libs.Analysis.SubsequencesMetric]
k:100 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:102 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:103 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
k:104 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:105 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
k:105 [binder, in Waterproof.Libs.Analysis.Subsequences]
k:107 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
K:107 [binder, in Waterproof.Libs.Analysis.SupAndInf]
k:108 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:11 [binder, in Waterproof.Libs.Analysis.SequentialAccumulationPoints]
k:11 [binder, in Waterproof.Libs.Analysis.Subsequences]
k:11 [binder, in Waterproof.Libs.Analysis.SubsequencesMetric]
k:112 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:114 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:114 [binder, in Waterproof.Libs.Analysis.Subsequences]
k:116 [binder, in Waterproof.Libs.Analysis.Subsequences]
k:12 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
k:12 [binder, in Waterproof.Libs.Analysis.SequentialAccumulationPoints]
k:120 [binder, in Waterproof.Libs.Analysis.Subsequences]
k:121 [binder, in Waterproof.Libs.Analysis.Subsequences]
k:122 [binder, in Waterproof.Libs.Analysis.Subsequences]
k:13 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:13 [binder, in Waterproof.Libs.Analysis.SequentialAccumulationPoints]
k:14 [binder, in Waterproof.Libs.Analysis.SequentialAccumulationPoints]
k:14 [binder, in Waterproof.Libs.Analysis.SequencesMetric]
k:15 [binder, in Waterproof.Libs.Analysis.SequentialAccumulationPoints]
k:15 [binder, in Waterproof.Libs.Analysis.Subsequences]
k:155 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
k:16 [binder, in Waterproof.Libs.Analysis.SequentialAccumulationPoints]
k:16 [binder, in Waterproof.Libs.Analysis.SubsequencesMetric]
k:162 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
k:166 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
k:168 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
k:170 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
k:176 [binder, in Waterproof.Libs.Analysis.SupAndInf]
k:178 [binder, in Waterproof.Libs.Analysis.SupAndInf]
K:18 [binder, in Waterproof.Libs.Analysis.Sequences]
k:185 [binder, in Waterproof.Libs.Analysis.SupAndInf]
k:19 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:19 [binder, in Waterproof.Libs.Analysis.SequentialAccumulationPoints]
k:19 [binder, in Waterproof.Libs.Analysis.SubsequencesMetric]
k:19 [binder, in Waterproof.Libs.Analysis.Series]
k:190 [binder, in Waterproof.Libs.Analysis.SupAndInf]
k:194 [binder, in Waterproof.Libs.Analysis.SupAndInf]
k:195 [binder, in Waterproof.Libs.Analysis.SupAndInf]
k:2 [binder, in Waterproof.Libs.Analysis.SubsequencesMetric]
k:2 [binder, in Waterproof.Libs.Analysis.Series]
k:20 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
k:21 [binder, in Waterproof.Libs.Analysis.Subsequences]
k:21 [binder, in Waterproof.Libs.Analysis.SubsequencesMetric]
k:23 [binder, in Waterproof.Libs.Analysis.SubsequencesMetric]
k:24 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
k:24 [binder, in Waterproof.Libs.Analysis.SubsequencesMetric]
k:25 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:25 [binder, in Waterproof.Libs.Analysis.Sequences]
k:26 [binder, in Waterproof.Libs.Analysis.SubsequencesMetric]
k:28 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:29 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
k:3 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
k:30 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
k:30 [binder, in Waterproof.Libs.Analysis.SubsequencesMetric]
k:31 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
k:31 [binder, in Waterproof.Libs.Analysis.Subsequences]
k:33 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:34 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:34 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
k:36 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:37 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:37 [binder, in Waterproof.Libs.Analysis.Subsequences]
k:37 [binder, in Waterproof.Libs.Analysis.SubsequencesMetric]
k:38 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:39 [binder, in Waterproof.Libs.Analysis.SubsequencesMetric]
k:4 [binder, in Waterproof.Libs.Analysis.SequentialAccumulationPoints]
k:4 [binder, in Waterproof.Libs.Analysis.SubsequencesMetric]
k:40 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:41 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:43 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:44 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
k:44 [binder, in Waterproof.Libs.Analysis.Subsequences]
k:44 [binder, in Waterproof.Libs.Analysis.SubsequencesMetric]
k:45 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:45 [binder, in Waterproof.Libs.Analysis.SubsequencesMetric]
k:46 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:46 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
k:46 [binder, in Waterproof.Libs.Analysis.Subsequences]
k:46 [binder, in Waterproof.Libs.Analysis.SubsequencesMetric]
k:47 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:48 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:49 [binder, in Waterproof.Libs.Analysis.Subsequences]
k:49 [binder, in Waterproof.Libs.Analysis.SubsequencesMetric]
k:5 [binder, in Waterproof.Libs.Analysis.Subsequences]
k:5 [binder, in Waterproof.Libs.Analysis.SubsequencesMetric]
k:5 [binder, in Waterproof.Libs.Analysis.Sequences]
K:50 [binder, in Waterproof.Libs.Analysis.SubsequencesMetric]
k:51 [binder, in Waterproof.Libs.Analysis.SubsequencesMetric]
k:52 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
k:53 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:55 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:57 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:57 [binder, in Waterproof.Libs.Analysis.Subsequences]
k:58 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:58 [binder, in Waterproof.Libs.Analysis.Subsequences]
k:59 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:59 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
k:6 [binder, in Waterproof.Libs.Analysis.SubsequencesMetric]
k:60 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:61 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:61 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
k:62 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:63 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:63 [binder, in Waterproof.Libs.Analysis.Subsequences]
k:64 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:64 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
k:65 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:65 [binder, in Waterproof.Libs.Analysis.Subsequences]
k:66 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:67 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:67 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
k:67 [binder, in Waterproof.Libs.Analysis.Subsequences]
k:68 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:68 [binder, in Waterproof.Libs.Analysis.Subsequences]
k:69 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:70 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:70 [binder, in Waterproof.Libs.Analysis.Subsequences]
k:72 [binder, in Waterproof.Libs.Analysis.Subsequences]
k:73 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
k:73 [binder, in Waterproof.Libs.Analysis.Subsequences]
k:74 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:76 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:76 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
k:76 [binder, in Waterproof.Libs.Analysis.Subsequences]
k:77 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:77 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
k:78 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:79 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:79 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
k:79 [binder, in Waterproof.Libs.Analysis.Subsequences]
k:8 [binder, in Waterproof.Libs.Analysis.Sequences]
k:81 [binder, in Waterproof.Libs.Analysis.Subsequences]
K:81 [binder, in Waterproof.Libs.Analysis.SupAndInf]
k:82 [binder, in Waterproof.Libs.Analysis.Subsequences]
k:84 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
k:85 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:85 [binder, in Waterproof.Libs.Analysis.Subsequences]
k:86 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:87 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
K:88 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:89 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
K:90 [binder, in Waterproof.Libs.Analysis.SupAndInf]
k:95 [binder, in Waterproof.Libs.Analysis.Subsequences]
k:96 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
k:98 [binder, in Waterproof.Libs.Analysis.Subsequences]
K:99 [binder, in Waterproof.Libs.Analysis.SupAndInf]

L

lcn:179 [binder, in Waterproof.Chains.Inequalities]
lcn:183 [binder, in Waterproof.Chains.Inequalities]
lcn:219 [binder, in Waterproof.Chains.Inequalities]
lcn:223 [binder, in Waterproof.Chains.Inequalities]
lcx:181 [binder, in Waterproof.Chains.Inequalities]
lcx:185 [binder, in Waterproof.Chains.Inequalities]
lcx:221 [binder, in Waterproof.Chains.Inequalities]
lcx:225 [binder, in Waterproof.Chains.Inequalities]
lc_map [definition, in Waterproof.Chains.Inequalities]
lc_interpretable [instance, in Waterproof.Chains.Inequalities]
lc_total_statement [definition, in Waterproof.Chains.Inequalities]
lc_weak_global_statement [definition, in Waterproof.Chains.Inequalities]
lc_global_statement [definition, in Waterproof.Chains.Inequalities]
lc_tail [definition, in Waterproof.Chains.Inequalities]
lc_head [definition, in Waterproof.Chains.Inequalities]
left [constructor, in Waterproof.Tactics.Either]
left_in_closed_open [lemma, in Waterproof.Libs.Reals]
LessChain [inductive, in Waterproof.Chains.Inequalities]
LessRel [inductive, in Waterproof.Chains.Inequalities]
less_rel_to_pred [projection, in Waterproof.Chains.Inequalities]
less_relation_flow [definition, in Waterproof.Chains.Inequalities]
limit_in_point [definition, in Waterproof.Libs.Analysis.ContinuityDomainR]
limit_in_point [definition, in Waterproof.Libs.Analysis.ContinuityDomainNat]
LimsupLiminfBolzano [library]
lim_sup_bdd_is_lub_seq_acc_pts [lemma, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
lim_const_min_1_over_n_plus_1 [lemma, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
lim_sup_bdd [definition, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
lim_d_0 [lemma, in Waterproof.Libs.Analysis.Sequences]
lim_const_seq [lemma, in Waterproof.Libs.Analysis.Sequences]
link_gc_grtr_R_Z [instance, in Waterproof.Chains.Inequalities]
link_gc_grtr_Z_R [instance, in Waterproof.Chains.Inequalities]
link_gc_eq_R_Z [instance, in Waterproof.Chains.Inequalities]
link_gc_eq_Z_R [instance, in Waterproof.Chains.Inequalities]
link_ec_grtr_R_Z [instance, in Waterproof.Chains.Inequalities]
link_ec_grtr_Z_R [instance, in Waterproof.Chains.Inequalities]
link_lc_less_R_Z [instance, in Waterproof.Chains.Inequalities]
link_lc_less_Z_R [instance, in Waterproof.Chains.Inequalities]
link_lc_eq_R_Z [instance, in Waterproof.Chains.Inequalities]
link_lc_eq_Z_R [instance, in Waterproof.Chains.Inequalities]
link_ec_less_R_Z [instance, in Waterproof.Chains.Inequalities]
link_ec_less_Z_R [instance, in Waterproof.Chains.Inequalities]
link_ec_eq_R_Z [instance, in Waterproof.Chains.Inequalities]
link_ec_eq_Z_R [instance, in Waterproof.Chains.Inequalities]
link_gc_grtr_R_nat [instance, in Waterproof.Chains.Inequalities]
link_gc_grtr_nat_R [instance, in Waterproof.Chains.Inequalities]
link_gc_eq_R_nat [instance, in Waterproof.Chains.Inequalities]
link_gc_eq_nat_R [instance, in Waterproof.Chains.Inequalities]
link_ec_grtr_R_nat [instance, in Waterproof.Chains.Inequalities]
link_ec_grtr_nat_R [instance, in Waterproof.Chains.Inequalities]
link_lc_less_R_nat [instance, in Waterproof.Chains.Inequalities]
link_lc_less_nat_R [instance, in Waterproof.Chains.Inequalities]
link_lc_eq_R_nat [instance, in Waterproof.Chains.Inequalities]
link_lc_eq_nat_R [instance, in Waterproof.Chains.Inequalities]
link_ec_less_R_nat [instance, in Waterproof.Chains.Inequalities]
link_ec_less_nat_R [instance, in Waterproof.Chains.Inequalities]
link_ec_eq_R_nat [instance, in Waterproof.Chains.Inequalities]
link_ec_eq_nat_R [instance, in Waterproof.Chains.Inequalities]
link_gc_grtr_inst [instance, in Waterproof.Chains.Inequalities]
link_gc_eq_inst [instance, in Waterproof.Chains.Inequalities]
link_ec_grtr_inst [instance, in Waterproof.Chains.Inequalities]
link_lc_less_inst [instance, in Waterproof.Chains.Inequalities]
link_lc_eq_inst [instance, in Waterproof.Chains.Inequalities]
link_ec_less_inst [instance, in Waterproof.Chains.Inequalities]
link_ec_eq_inst [instance, in Waterproof.Chains.Inequalities]
link_gc_grtr [constructor, in Waterproof.Chains.Inequalities]
link_gc_eq [constructor, in Waterproof.Chains.Inequalities]
link_ec_grtr [constructor, in Waterproof.Chains.Inequalities]
link_lc_less [constructor, in Waterproof.Chains.Inequalities]
link_lc_eq [constructor, in Waterproof.Chains.Inequalities]
link_ec_less [constructor, in Waterproof.Chains.Inequalities]
link_ec_eq [constructor, in Waterproof.Chains.Inequalities]
ln:166 [binder, in Waterproof.Chains.Inequalities]
ln:170 [binder, in Waterproof.Chains.Inequalities]
ln:174 [binder, in Waterproof.Chains.Inequalities]
ln:178 [binder, in Waterproof.Chains.Inequalities]
ln:182 [binder, in Waterproof.Chains.Inequalities]
ln:186 [binder, in Waterproof.Chains.Inequalities]
ln:190 [binder, in Waterproof.Chains.Inequalities]
ln:194 [binder, in Waterproof.Chains.Inequalities]
ln:198 [binder, in Waterproof.Chains.Inequalities]
ln:202 [binder, in Waterproof.Chains.Inequalities]
ln:206 [binder, in Waterproof.Chains.Inequalities]
ln:210 [binder, in Waterproof.Chains.Inequalities]
ln:214 [binder, in Waterproof.Chains.Inequalities]
ln:218 [binder, in Waterproof.Chains.Inequalities]
ln:222 [binder, in Waterproof.Chains.Inequalities]
ln:226 [binder, in Waterproof.Chains.Inequalities]
ln:230 [binder, in Waterproof.Chains.Inequalities]
ln:234 [binder, in Waterproof.Chains.Inequalities]
ln:238 [binder, in Waterproof.Chains.Inequalities]
ln:242 [binder, in Waterproof.Chains.Inequalities]
low_bd_seq_is_low_bd_lim [lemma, in Waterproof.Libs.Analysis.Sequences]
low_bd_set_opp_to_upp_bd_set [lemma, in Waterproof.Libs.Analysis.SupAndInf]
low_bd_set_to_upp_bd_set_opp [lemma, in Waterproof.Libs.Analysis.SupAndInf]
lx:164 [binder, in Waterproof.Chains.Inequalities]
lx:168 [binder, in Waterproof.Chains.Inequalities]
lx:172 [binder, in Waterproof.Chains.Inequalities]
lx:176 [binder, in Waterproof.Chains.Inequalities]
lx:184 [binder, in Waterproof.Chains.Inequalities]
lx:188 [binder, in Waterproof.Chains.Inequalities]
lx:192 [binder, in Waterproof.Chains.Inequalities]
lx:200 [binder, in Waterproof.Chains.Inequalities]
lx:204 [binder, in Waterproof.Chains.Inequalities]
lx:208 [binder, in Waterproof.Chains.Inequalities]
lx:212 [binder, in Waterproof.Chains.Inequalities]
lx:216 [binder, in Waterproof.Chains.Inequalities]
lx:224 [binder, in Waterproof.Chains.Inequalities]
lx:228 [binder, in Waterproof.Chains.Inequalities]
lx:232 [binder, in Waterproof.Chains.Inequalities]
lx:240 [binder, in Waterproof.Chains.Inequalities]
l:10 [binder, in Waterproof.Libs.Analysis.Series]
l:101 [binder, in Waterproof.Libs.Analysis.Subsequences]
L:106 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
l:109 [binder, in Waterproof.Libs.Analysis.Subsequences]
l:12 [binder, in Waterproof.Libs.Analysis.Sequences]
l:12 [binder, in Waterproof.Libs.Analysis.Series]
l:14 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
l:147 [binder, in Waterproof.Libs.Analysis.SupAndInf]
l:148 [binder, in Waterproof.Libs.Analysis.SupAndInf]
l:15 [binder, in Waterproof.Libs.Analysis.SupAndInf]
l:157 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
l:157 [binder, in Waterproof.Libs.Analysis.SupAndInf]
l:158 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
l:158 [binder, in Waterproof.Libs.Analysis.SupAndInf]
l:159 [binder, in Waterproof.Libs.Analysis.SupAndInf]
l:16 [binder, in Waterproof.Libs.Analysis.Subsequences]
l:16 [binder, in Waterproof.Libs.Analysis.Series]
l:171 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
l:20 [binder, in Waterproof.Libs.Analysis.Series]
L:21 [binder, in Waterproof.Libs.Analysis.Series]
l:22 [binder, in Waterproof.Libs.Analysis.SubsequencesMetric]
l:22 [binder, in Waterproof.Libs.Analysis.Sequences]
L:22 [binder, in Waterproof.Libs.Analysis.ContinuityDomainNat]
l:23 [binder, in Waterproof.Libs.Analysis.Subsequences]
l:25 [binder, in Waterproof.Libs.Analysis.SubsequencesMetric]
l:3 [binder, in Waterproof.Libs.Analysis.Series]
l:36 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
l:38 [binder, in Waterproof.Libs.Analysis.SupAndInf]
l:40 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
l:41 [binder, in Waterproof.Libs.Analysis.SupAndInf]
l:45 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
l:47 [binder, in Waterproof.Libs.Analysis.Sequences]
l:54 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
l:56 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
L:56 [binder, in Waterproof.Libs.Analysis.SupAndInf]
L:58 [binder, in Waterproof.Libs.Analysis.Sequences]
l:6 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
l:62 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
l:63 [binder, in Waterproof.Libs.Analysis.SupAndInf]
l:65 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
l:66 [binder, in Waterproof.Libs.Analysis.Subsequences]
L:67 [binder, in Waterproof.Libs.Analysis.SupAndInf]
L:68 [binder, in Waterproof.Libs.Analysis.Sequences]
l:69 [binder, in Waterproof.Libs.Analysis.Subsequences]
l:73 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
L:73 [binder, in Waterproof.Libs.Analysis.SupAndInf]
l:77 [binder, in Waterproof.Libs.Analysis.Sequences]
L:79 [binder, in Waterproof.Libs.Analysis.SupAndInf]
l:80 [binder, in Waterproof.Libs.Analysis.Subsequences]
l:81 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
l:82 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
L:82 [binder, in Waterproof.Libs.Analysis.SupAndInf]
l:83 [binder, in Waterproof.Libs.Analysis.Subsequences]
l:86 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
l:88 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
L:88 [binder, in Waterproof.Libs.Analysis.SupAndInf]
l:89 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
l:9 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
l:90 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
l:90 [binder, in Waterproof.Libs.Analysis.Subsequences]
l:91 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
L:91 [binder, in Waterproof.Libs.Analysis.SupAndInf]
l:92 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
l:97 [binder, in Waterproof.Libs.Analysis.Subsequences]
l:98 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
l:99 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
l:99 [binder, in Waterproof.Libs.Analysis.Subsequences]

M

make_sumtriad_uninformative_6 [lemma, in Waterproof.Libs.Logic.ConstructiveLogic]
make_sumtriad_uninformative_5 [lemma, in Waterproof.Libs.Logic.ConstructiveLogic]
make_sumtriad_uninformative_4 [lemma, in Waterproof.Libs.Logic.ConstructiveLogic]
make_sumtriad_uninformative_3 [lemma, in Waterproof.Libs.Logic.ConstructiveLogic]
make_sumtriad_uninformative_2 [lemma, in Waterproof.Libs.Logic.ConstructiveLogic]
make_sumtriad_uninformative_1 [lemma, in Waterproof.Libs.Logic.ConstructiveLogic]
make_sumbool_uninformative_2 [lemma, in Waterproof.Libs.Logic.ConstructiveLogic]
make_sumbool_uninformative_1 [lemma, in Waterproof.Libs.Logic.ConstructiveLogic]
Manipulation [library]
max_or_strict [lemma, in Waterproof.Libs.Analysis.SupAndInf]
MessagesToUser [library]
metricspace [section, in Waterproof.Libs.Analysis.ContinuityDomainNat]
MetricSpaces [library]
metricspace.X [variable, in Waterproof.Libs.Analysis.ContinuityDomainNat]
middle [constructor, in Waterproof.Tactics.Either]
min_1_over_n_plus_1_to_0 [lemma, in Waterproof.Libs.Analysis.Sequences]
mouse_tail [lemma, in Waterproof.Libs.Analysis.Series]
my_section.X [variable, in Waterproof.Libs.Analysis.SubsequencesMetric]
my_section [section, in Waterproof.Libs.Analysis.SubsequencesMetric]
m_seq:56 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
M0:131 [binder, in Waterproof.Libs.Analysis.SupAndInf]
M0:132 [binder, in Waterproof.Libs.Analysis.SupAndInf]
M0:139 [binder, in Waterproof.Libs.Analysis.SupAndInf]
M0:140 [binder, in Waterproof.Libs.Analysis.SupAndInf]
M0:36 [binder, in Waterproof.Libs.Analysis.SupAndInf]
M0:37 [binder, in Waterproof.Libs.Analysis.SupAndInf]
M0:42 [binder, in Waterproof.Libs.Analysis.SupAndInf]
M0:53 [binder, in Waterproof.Libs.Analysis.SupAndInf]
M0:57 [binder, in Waterproof.Libs.Analysis.SupAndInf]
M0:60 [binder, in Waterproof.Libs.Analysis.SupAndInf]
M0:64 [binder, in Waterproof.Libs.Analysis.SupAndInf]
M1:101 [binder, in Waterproof.Libs.Analysis.Sequences]
M1:108 [binder, in Waterproof.Libs.Analysis.Sequences]
M1:99 [binder, in Waterproof.Libs.Analysis.Sequences]
M:1 [binder, in Waterproof.Libs.Analysis.SequencesMetric]
m:10 [binder, in Waterproof.Libs.Analysis.SubsequencesMetric]
M:10 [binder, in Waterproof.Libs.Analysis.SequencesMetric]
m:10 [binder, in Waterproof.Libs.Analysis.ContinuityDomainNat]
m:104 [binder, in Waterproof.Libs.Analysis.SupAndInf]
M:105 [binder, in Waterproof.Libs.Analysis.Sequences]
m:109 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
m:11 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
M:112 [binder, in Waterproof.Libs.Analysis.SupAndInf]
M:113 [binder, in Waterproof.Libs.Analysis.Sequences]
m:115 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
m:116 [binder, in Waterproof.Libs.Analysis.SupAndInf]
M:117 [binder, in Waterproof.Libs.Analysis.Sequences]
m:12 [binder, in Waterproof.Libs.Analysis.Subsequences]
m:12 [binder, in Waterproof.Libs.Analysis.SupAndInf]
m:12 [binder, in Waterproof.Libs.Analysis.ContinuityDomainNat]
m:120 [binder, in Waterproof.Libs.Analysis.Sequences]
M:120 [binder, in Waterproof.Libs.Analysis.SupAndInf]
M:123 [binder, in Waterproof.Libs.Analysis.Sequences]
m:124 [binder, in Waterproof.Libs.Analysis.SupAndInf]
M:127 [binder, in Waterproof.Libs.Analysis.Sequences]
M:128 [binder, in Waterproof.Libs.Analysis.SupAndInf]
m:14 [binder, in Waterproof.Libs.Analysis.SubsequencesMetric]
M:14 [binder, in Waterproof.Libs.Analysis.Sequences]
m:14 [binder, in Waterproof.Libs.Analysis.SupAndInf]
m:144 [binder, in Waterproof.Libs.Analysis.SupAndInf]
M:161 [binder, in Waterproof.Libs.Analysis.SupAndInf]
M:168 [binder, in Waterproof.Libs.Analysis.SupAndInf]
m:17 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
m:17 [binder, in Waterproof.Libs.Analysis.Subsequences]
m:171 [binder, in Waterproof.Libs.Analysis.SupAndInf]
m:184 [binder, in Waterproof.Libs.Analysis.SupAndInf]
m:188 [binder, in Waterproof.Libs.Analysis.SupAndInf]
M:19 [binder, in Waterproof.Libs.Analysis.SupAndInf]
m:192 [binder, in Waterproof.Libs.Analysis.SupAndInf]
m:2 [binder, in Waterproof.Libs.Analysis.ContinuityDomainNat]
m:22 [binder, in Waterproof.Libs.Analysis.SupAndInf]
m:25 [binder, in Waterproof.Libs.Analysis.SupAndInf]
m:26 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
m:27 [binder, in Waterproof.Libs.Analysis.Subsequences]
m:29 [binder, in Waterproof.Libs.Analysis.Subsequences]
M:29 [binder, in Waterproof.Libs.Analysis.SupAndInf]
m:3 [binder, in Waterproof.Libs.Analysis.Subsequences]
m:3 [binder, in Waterproof.Libs.Analysis.ContinuityDomainNat]
M:31 [binder, in Waterproof.Libs.Analysis.Series]
M:32 [binder, in Waterproof.Libs.Analysis.SupAndInf]
m:33 [binder, in Waterproof.Libs.Analysis.SupAndInf]
m:35 [binder, in Waterproof.Libs.Analysis.Subsequences]
M:35 [binder, in Waterproof.Libs.Analysis.SupAndInf]
m:38 [binder, in Waterproof.Libs.Analysis.Subsequences]
M:4 [binder, in Waterproof.Libs.Analysis.Series]
m:42 [binder, in Waterproof.Libs.Analysis.Subsequences]
m:43 [binder, in Waterproof.Libs.Analysis.SubsequencesMetric]
M:45 [binder, in Waterproof.Libs.Analysis.Series]
m:46 [binder, in Waterproof.Libs.Analysis.SupAndInf]
m:47 [binder, in Waterproof.Libs.Analysis.Subsequences]
m:48 [binder, in Waterproof.Libs.Analysis.SupAndInf]
M:49 [binder, in Waterproof.Libs.Analysis.SupAndInf]
M:5 [binder, in Waterproof.Libs.Analysis.SupAndInf]
m:5 [binder, in Waterproof.Libs.Analysis.ContinuityDomainNat]
m:51 [binder, in Waterproof.Libs.Analysis.Subsequences]
M:51 [binder, in Waterproof.Libs.Analysis.SupAndInf]
m:53 [binder, in Waterproof.Libs.Analysis.Subsequences]
m:54 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
m:55 [binder, in Waterproof.Libs.Analysis.Subsequences]
M:55 [binder, in Waterproof.Libs.Analysis.SupAndInf]
M:56 [binder, in Waterproof.Libs.Analysis.Subsequences]
m:59 [binder, in Waterproof.Libs.Analysis.Subsequences]
M:59 [binder, in Waterproof.Libs.Analysis.Sequences]
m:59 [binder, in Waterproof.Libs.Analysis.SupAndInf]
m:6 [binder, in Waterproof.Libs.Analysis.SequentialAccumulationPoints]
M:60 [binder, in Waterproof.Libs.Analysis.Subsequences]
M:61 [binder, in Waterproof.Libs.Analysis.Subsequences]
m:62 [binder, in Waterproof.Libs.Analysis.SupAndInf]
M:66 [binder, in Waterproof.Libs.Analysis.SupAndInf]
M:69 [binder, in Waterproof.Libs.Analysis.Sequences]
m:7 [binder, in Waterproof.Libs.Analysis.SequentialAccumulationPoints]
m:7 [binder, in Waterproof.Libs.Analysis.Subsequences]
M:7 [binder, in Waterproof.Libs.Analysis.SupAndInf]
m:72 [binder, in Waterproof.Libs.Analysis.SupAndInf]
m:76 [binder, in Waterproof.Libs.Analysis.Sequences]
M:78 [binder, in Waterproof.Libs.Analysis.SupAndInf]
m:8 [binder, in Waterproof.Libs.Analysis.ContinuityDomainNat]
m:83 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
m:87 [binder, in Waterproof.Libs.Analysis.SupAndInf]
M:9 [binder, in Waterproof.Libs.Analysis.SequentialAccumulationPoints]
m:9 [binder, in Waterproof.Libs.Analysis.Subsequences]
m:9 [binder, in Waterproof.Libs.Analysis.SupAndInf]
M:92 [binder, in Waterproof.Libs.Analysis.Sequences]
m:95 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
M:95 [binder, in Waterproof.Libs.Analysis.Sequences]
M:96 [binder, in Waterproof.Libs.Analysis.SupAndInf]

N

NaturalInduction [module, in Waterproof.Util.Goals]
NaturalInduction.Base [module, in Waterproof.Util.Goals]
NaturalInduction.Base.unwrap [definition, in Waterproof.Util.Goals]
NaturalInduction.Base.wrap [constructor, in Waterproof.Util.Goals]
NaturalInduction.Base.Wrapper [inductive, in Waterproof.Util.Goals]
NaturalInduction.Step [module, in Waterproof.Util.Goals]
NaturalInduction.Step.unwrap [definition, in Waterproof.Util.Goals]
NaturalInduction.Step.wrap [constructor, in Waterproof.Util.Goals]
NaturalInduction.Step.Wrapper [inductive, in Waterproof.Util.Goals]
nat_dist_less_than_one_iff_equal [lemma, in Waterproof.Libs.Analysis.ContinuityDomainNat]
nat_dist_larger_zero_not_equal [lemma, in Waterproof.Libs.Analysis.ContinuityDomainNat]
nat_not_equal_dist_larger_one [lemma, in Waterproof.Libs.Analysis.ContinuityDomainNat]
Na:53 [binder, in Waterproof.Libs.Analysis.Sequences]
Nc:55 [binder, in Waterproof.Libs.Analysis.Sequences]
Negation [library]
Nn:193 [binder, in Waterproof.Libs.Analysis.SupAndInf]
Nn:22 [binder, in Waterproof.Libs.Analysis.Series]
Nn:23 [binder, in Waterproof.Libs.Analysis.Series]
Nn:24 [binder, in Waterproof.Libs.Analysis.Series]
Nn:25 [binder, in Waterproof.Libs.Analysis.Series]
Nn:26 [binder, in Waterproof.Libs.Analysis.Series]
Nn:28 [binder, in Waterproof.Libs.Analysis.Series]
Nn:29 [binder, in Waterproof.Libs.Analysis.Series]
Nn:30 [binder, in Waterproof.Libs.Analysis.Series]
Nn:31 [binder, in Waterproof.Libs.Analysis.Sequences]
Nn:33 [binder, in Waterproof.Libs.Analysis.Series]
Nn:34 [binder, in Waterproof.Libs.Analysis.Series]
Nn:35 [binder, in Waterproof.Libs.Analysis.Series]
Nn:36 [binder, in Waterproof.Libs.Analysis.Series]
Nn:37 [binder, in Waterproof.Libs.Analysis.Series]
Nn:38 [binder, in Waterproof.Libs.Analysis.Series]
Nn:39 [binder, in Waterproof.Libs.Analysis.Series]
Nn:40 [binder, in Waterproof.Libs.Analysis.Series]
Nn:43 [binder, in Waterproof.Libs.Analysis.Series]
Nn:44 [binder, in Waterproof.Libs.Analysis.Series]
Nn:51 [binder, in Waterproof.Libs.Analysis.Sequences]
Nn:65 [binder, in Waterproof.Libs.Analysis.Sequences]
Notations [library]
not_neg_pos_func [lemma, in Waterproof.Libs.Negation]
not_ex_all_func [lemma, in Waterproof.Libs.Negation]
not_all_ex_func [lemma, in Waterproof.Libs.Negation]
not_impl_and_func [lemma, in Waterproof.Libs.Negation]
not_and_impl_func [lemma, in Waterproof.Libs.Negation]
not_and_or_func [lemma, in Waterproof.Libs.Negation]
not_or_and_func [lemma, in Waterproof.Libs.Negation]
not_in_compl_implies_in [lemma, in Waterproof.Libs.Analysis.OpenAndClosed]
n_kplus1:159 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
n_0:153 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
n_kplus1:100 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
n_0:94 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
n_kplus1:87 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
n_kplus1:83 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
n_ge_k:16 [binder, in Waterproof.Libs.Analysis.SequencesMetric]
n0:163 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
n0:164 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
N0:36 [binder, in Waterproof.Libs.Analysis.SubsequencesMetric]
n0:75 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
N1:124 [binder, in Waterproof.Libs.Analysis.Sequences]
N1:128 [binder, in Waterproof.Libs.Analysis.Sequences]
N1:16 [binder, in Waterproof.Libs.Analysis.Sequences]
N1:38 [binder, in Waterproof.Libs.Analysis.SubsequencesMetric]
n1:38 [binder, in Waterproof.Libs.Analysis.Sequences]
N1:5 [binder, in Waterproof.Libs.Analysis.SequencesMetric]
N1:86 [binder, in Waterproof.Libs.Analysis.Sequences]
N2:88 [binder, in Waterproof.Libs.Analysis.Sequences]
N3:48 [binder, in Waterproof.Libs.Analysis.SubsequencesMetric]
n:1 [binder, in Waterproof.Tactics.Induction]
n:1 [binder, in Waterproof.Libs.Analysis.SubsequencesMetric]
n:1 [binder, in Waterproof.Libs.Analysis.Sequences]
n:1 [binder, in Waterproof.Libs.Analysis.ContinuityDomainNat]
n:10 [binder, in Waterproof.Libs.Analysis.SequentialAccumulationPoints]
N:10 [binder, in Waterproof.Libs.Analysis.Subsequences]
n:100 [binder, in Waterproof.Libs.Analysis.Sequences]
n:101 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
n:102 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
n:102 [binder, in Waterproof.Libs.Analysis.Sequences]
n:103 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
n:103 [binder, in Waterproof.Libs.Analysis.Sequences]
n:104 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
n:104 [binder, in Waterproof.Libs.Analysis.Sequences]
n:106 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
n:106 [binder, in Waterproof.Libs.Analysis.Sequences]
N:107 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
n:107 [binder, in Waterproof.Libs.Analysis.Subsequences]
n:107 [binder, in Waterproof.Libs.Analysis.Sequences]
n:109 [binder, in Waterproof.Libs.Analysis.Sequences]
n:11 [binder, in Waterproof.Libs.Analysis.SequencesMetric]
n:11 [binder, in Waterproof.Libs.Analysis.ContinuityDomainNat]
n:110 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
n:110 [binder, in Waterproof.Libs.Analysis.Sequences]
N:111 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
n:111 [binder, in Waterproof.Libs.Analysis.Sequences]
N:113 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
n:113 [binder, in Waterproof.Libs.Analysis.Subsequences]
n:114 [binder, in Waterproof.Libs.Analysis.Sequences]
n:115 [binder, in Waterproof.Libs.Analysis.Sequences]
n:116 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
n:118 [binder, in Waterproof.Libs.Analysis.Sequences]
n:121 [binder, in Waterproof.Libs.Analysis.Sequences]
n:125 [binder, in Waterproof.Libs.Analysis.Sequences]
n:129 [binder, in Waterproof.Libs.Analysis.Sequences]
N:14 [binder, in Waterproof.Libs.Analysis.Subsequences]
n:14 [binder, in Waterproof.Libs.Analysis.Series]
n:15 [binder, in Waterproof.Libs.Analysis.SubsequencesMetric]
n:15 [binder, in Waterproof.Libs.Analysis.Sequences]
n:15 [binder, in Waterproof.Libs.Analysis.SequencesMetric]
n:156 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
n:16 [binder, in Waterproof.Libs.Analysis.ContinuityDomainNat]
n:161 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
n:163 [binder, in Waterproof.Chains.Inequalities]
n:165 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
n:167 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
n:169 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
n:17 [binder, in Waterproof.Libs.Analysis.SubsequencesMetric]
n:17 [binder, in Waterproof.Libs.Analysis.Sequences]
n:17 [binder, in Waterproof.Libs.Analysis.Series]
n:171 [binder, in Waterproof.Chains.Inequalities]
n:181 [binder, in Waterproof.Libs.Analysis.SupAndInf]
n:187 [binder, in Waterproof.Chains.Inequalities]
N:189 [binder, in Waterproof.Libs.Analysis.SupAndInf]
N:19 [binder, in Waterproof.Libs.Analysis.Subsequences]
n:19 [binder, in Waterproof.Libs.Analysis.Sequences]
n:19 [binder, in Waterproof.Libs.Analysis.ContinuityDomainNat]
n:2 [binder, in Waterproof.Libs.Analysis.Sequences]
n:20 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
n:20 [binder, in Waterproof.Libs.Analysis.Subsequences]
n:203 [binder, in Waterproof.Chains.Inequalities]
n:211 [binder, in Waterproof.Chains.Inequalities]
n:227 [binder, in Waterproof.Chains.Inequalities]
n:23 [binder, in Waterproof.Libs.Analysis.Sequences]
n:24 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
n:24 [binder, in Waterproof.Libs.Analysis.Sequences]
n:25 [binder, in Waterproof.Libs.Analysis.ContinuityDomainNat]
n:26 [binder, in Waterproof.Libs.Analysis.Sequences]
n:27 [binder, in Waterproof.Libs.Analysis.SubsequencesMetric]
N:27 [binder, in Waterproof.Libs.Analysis.Series]
N:28 [binder, in Waterproof.Libs.Analysis.Subsequences]
n:28 [binder, in Waterproof.Libs.Analysis.Sequences]
n:3 [binder, in Waterproof.Libs.Analysis.SequentialAccumulationPoints]
n:3 [binder, in Waterproof.Libs.Analysis.SubsequencesMetric]
N:30 [binder, in Waterproof.Libs.Analysis.Subsequences]
n:31 [binder, in Waterproof.Libs.Analysis.SubsequencesMetric]
n:32 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
n:32 [binder, in Waterproof.Libs.Analysis.Sequences]
n:32 [binder, in Waterproof.Libs.Analysis.Series]
n:33 [binder, in Waterproof.Libs.Analysis.Sequences]
n:34 [binder, in Waterproof.Libs.Analysis.SubsequencesMetric]
n:34 [binder, in Waterproof.Libs.Analysis.Sequences]
N:36 [binder, in Waterproof.Libs.Analysis.Subsequences]
N:36 [binder, in Waterproof.Libs.Analysis.Sequences]
n:37 [binder, in Waterproof.Libs.Analysis.Sequences]
N:39 [binder, in Waterproof.Libs.Analysis.Subsequences]
n:39 [binder, in Waterproof.Libs.Analysis.Sequences]
N:4 [binder, in Waterproof.Notations.Reals]
N:4 [binder, in Waterproof.Libs.Analysis.Subsequences]
n:4 [binder, in Waterproof.Libs.Analysis.Sequences]
n:4 [binder, in Waterproof.Libs.Analysis.ContinuityDomainNat]
n:40 [binder, in Waterproof.Libs.Analysis.Sequences]
n:41 [binder, in Waterproof.Libs.Analysis.Sequences]
N:41 [binder, in Waterproof.Libs.Analysis.Series]
n:42 [binder, in Waterproof.Libs.Analysis.Sequences]
N:42 [binder, in Waterproof.Libs.Analysis.Series]
n:43 [binder, in Waterproof.Libs.Analysis.Sequences]
n:44 [binder, in Waterproof.Libs.Analysis.ContinuityDomainNat]
n:45 [binder, in Waterproof.Libs.Analysis.Subsequences]
n:45 [binder, in Waterproof.Libs.Analysis.ContinuityDomainNat]
n:46 [binder, in Waterproof.Libs.Analysis.Series]
n:47 [binder, in Waterproof.Libs.Analysis.Series]
N:48 [binder, in Waterproof.Libs.Analysis.Subsequences]
n:48 [binder, in Waterproof.Libs.Analysis.Sequences]
n:48 [binder, in Waterproof.Libs.Analysis.Series]
n:49 [binder, in Waterproof.Libs.Analysis.Sequences]
n:49 [binder, in Waterproof.Libs.Analysis.Series]
n:5 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
n:5 [binder, in Waterproof.Notations.Reals]
n:50 [binder, in Waterproof.Libs.Analysis.Series]
N:51 [binder, in Waterproof.Libs.Analysis.Series]
n:52 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
N:52 [binder, in Waterproof.Libs.Analysis.Subsequences]
n:52 [binder, in Waterproof.Libs.Analysis.Sequences]
N:52 [binder, in Waterproof.Libs.Analysis.Series]
N:54 [binder, in Waterproof.Libs.Analysis.Subsequences]
n:54 [binder, in Waterproof.Libs.Analysis.Sequences]
n:56 [binder, in Waterproof.Libs.Analysis.Sequences]
n:6 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
n:6 [binder, in Waterproof.Libs.Analysis.SequencesMetric]
n:6 [binder, in Waterproof.Libs.Analysis.Series]
n:6 [binder, in Waterproof.Libs.Analysis.ContinuityDomainNat]
n:60 [binder, in Waterproof.Libs.Analysis.Sequences]
n:61 [binder, in Waterproof.Libs.Analysis.Sequences]
N:63 [binder, in Waterproof.Libs.Analysis.Sequences]
n:64 [binder, in Waterproof.Libs.Analysis.Sequences]
n:66 [binder, in Waterproof.Libs.Analysis.Sequences]
n:68 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
n:7 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
n:7 [binder, in Waterproof.Libs.Analysis.Series]
n:7 [binder, in Waterproof.Libs.Analysis.ContinuityDomainNat]
n:70 [binder, in Waterproof.Libs.Analysis.Sequences]
n:71 [binder, in Waterproof.Libs.Analysis.Subsequences]
n:71 [binder, in Waterproof.Libs.Analysis.Sequences]
n:72 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
n:72 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
n:72 [binder, in Waterproof.Libs.Analysis.Sequences]
n:73 [binder, in Waterproof.Libs.Analysis.Sequences]
n:75 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
n:75 [binder, in Waterproof.Libs.Analysis.Subsequences]
n:78 [binder, in Waterproof.Libs.Analysis.Subsequences]
n:78 [binder, in Waterproof.Libs.Analysis.Sequences]
n:79 [binder, in Waterproof.Libs.Analysis.Sequences]
N:8 [binder, in Waterproof.Libs.Analysis.Subsequences]
n:8 [binder, in Waterproof.Libs.Analysis.Series]
n:80 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
N:81 [binder, in Waterproof.Libs.Analysis.Sequences]
n:82 [binder, in Waterproof.Libs.Analysis.Sequences]
n:84 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
N:84 [binder, in Waterproof.Libs.Analysis.Sequences]
n:85 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
n:85 [binder, in Waterproof.Libs.Analysis.Sequences]
N:86 [binder, in Waterproof.Libs.Analysis.Subsequences]
n:87 [binder, in Waterproof.Libs.Analysis.Sequences]
n:89 [binder, in Waterproof.Libs.Analysis.Sequences]
n:9 [binder, in Waterproof.Libs.Analysis.Sequences]
n:9 [binder, in Waterproof.Libs.Analysis.ContinuityDomainNat]
N:91 [binder, in Waterproof.Libs.Analysis.Subsequences]
n:93 [binder, in Waterproof.Libs.Analysis.Sequences]
N:94 [binder, in Waterproof.Libs.Analysis.Subsequences]
n:96 [binder, in Waterproof.Libs.Analysis.Sequences]
n:97 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
n:99 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
N₀:12 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
N₀:18 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
N₀:31 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
N₀:43 [binder, in Waterproof.Libs.Analysis.Subsequences]

O

Obtain [library]
one_in_complement_interval_closed_zero_open_one [lemma, in Waterproof.Libs.Analysis.OpenAndClosed]
OpenAndClosed [library]
open_ball [definition, in Waterproof.Libs.Analysis.OpenAndClosed]
OrderInterpretation [record, in Waterproof.Chains.Inequalities]
OrderInterpretation0:102 [binder, in Waterproof.Chains.Inequalities]
OrderInterpretation0:105 [binder, in Waterproof.Chains.Inequalities]
OrderInterpretation0:110 [binder, in Waterproof.Chains.Inequalities]
OrderInterpretation0:112 [binder, in Waterproof.Chains.Inequalities]
OrderInterpretation0:115 [binder, in Waterproof.Chains.Inequalities]
OrderInterpretation0:118 [binder, in Waterproof.Chains.Inequalities]
OrderInterpretation0:123 [binder, in Waterproof.Chains.Inequalities]
OrderInterpretation0:99 [binder, in Waterproof.Chains.Inequalities]
order_interpretation_R [instance, in Waterproof.Chains.Inequalities]
order_interpretation_nat [instance, in Waterproof.Chains.Inequalities]
or_not_and_func [lemma, in Waterproof.Libs.Negation]
or_func [lemma, in Waterproof.Libs.Negation]

P

partial_sums_pos_incr [lemma, in Waterproof.Libs.Analysis.Series]
partial_sums [abbreviation, in Waterproof.Libs.Analysis.Series]
pos_not_neg_func [lemma, in Waterproof.Libs.Negation]
pred [projection, in Waterproof.Notations.Sets]
prev:21 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
prev:53 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
pr1:2 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
pr2:3 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
pr:174 [binder, in Waterproof.Libs.Analysis.SupAndInf]
pr:183 [binder, in Waterproof.Libs.Analysis.SupAndInf]
pr:187 [binder, in Waterproof.Libs.Analysis.SupAndInf]
pr:191 [binder, in Waterproof.Libs.Analysis.SupAndInf]
P:1 [binder, in Waterproof.Libs.Logic.InformativeEpsilon]
P:1 [binder, in Waterproof.Libs.Logic.ConstructiveLogic]
p:1 [binder, in Waterproof.Libs.Analysis.OpenAndClosed]
P:11 [binder, in Waterproof.Libs.Logic.ConstructiveLogic]
P:113 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
p:12 [binder, in Waterproof.Libs.Analysis.SubsequencesMetric]
P:14 [binder, in Waterproof.Libs.Negation]
P:14 [binder, in Waterproof.Libs.Logic.ConstructiveLogic]
P:16 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
P:17 [binder, in Waterproof.Libs.Logic.ConstructiveLogic]
P:2 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
P:2 [binder, in Waterproof.Libs.Analysis.Subsequences]
P:20 [binder, in Waterproof.Libs.Negation]
P:20 [binder, in Waterproof.Libs.Logic.ConstructiveLogic]
P:3 [binder, in Waterproof.Libs.Logic.ConstructiveLogic]
P:33 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
p:33 [binder, in Waterproof.Libs.Analysis.SubsequencesMetric]
P:34 [binder, in Waterproof.Libs.Analysis.Subsequences]
P:38 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
P:41 [binder, in Waterproof.Libs.Analysis.Subsequences]
P:42 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
p:42 [binder, in Waterproof.Libs.Analysis.SubsequencesMetric]
P:48 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
P:5 [binder, in Waterproof.Libs.Logic.ConstructiveLogic]
P:54 [binder, in Waterproof.Libs.Negation]
P:60 [binder, in Waterproof.Libs.Negation]
P:66 [binder, in Waterproof.Libs.Negation]
P:72 [binder, in Waterproof.Libs.Negation]
P:8 [binder, in Waterproof.Libs.Logic.ConstructiveLogic]
P:93 [binder, in Waterproof.Libs.Analysis.Subsequences]

Q

quant_over_start_dep_only_on_start [lemma, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
q:112 [binder, in Waterproof.Libs.Analysis.Sequences]
Q:12 [binder, in Waterproof.Libs.Logic.ConstructiveLogic]
Q:15 [binder, in Waterproof.Libs.Negation]
Q:15 [binder, in Waterproof.Libs.Logic.ConstructiveLogic]
Q:152 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
Q:18 [binder, in Waterproof.Libs.Logic.ConstructiveLogic]
Q:2 [binder, in Waterproof.Libs.Logic.InformativeEpsilon]
Q:2 [binder, in Waterproof.Libs.Logic.ConstructiveLogic]
Q:21 [binder, in Waterproof.Libs.Negation]
Q:21 [binder, in Waterproof.Libs.Logic.ConstructiveLogic]
Q:4 [binder, in Waterproof.Libs.Logic.ConstructiveLogic]
Q:55 [binder, in Waterproof.Libs.Negation]
Q:6 [binder, in Waterproof.Libs.Logic.ConstructiveLogic]
Q:61 [binder, in Waterproof.Libs.Negation]
Q:66 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
Q:67 [binder, in Waterproof.Libs.Negation]
Q:70 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
Q:71 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
Q:73 [binder, in Waterproof.Libs.Negation]
Q:74 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
Q:78 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
Q:9 [binder, in Waterproof.Libs.Logic.ConstructiveLogic]
q:9 [binder, in Waterproof.Libs.Analysis.SequencesMetric]
q:9 [binder, in Waterproof.Libs.Analysis.ContinuityDomainR]
q:91 [binder, in Waterproof.Libs.Analysis.Sequences]
Q:93 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
q:98 [binder, in Waterproof.Libs.Analysis.Sequences]

R

Rabs_left1_with_minus [lemma, in Waterproof.Libs.Reals]
Rabs_zero [lemma, in Waterproof.Libs.Reals]
Rabs_m_lt_n [lemma, in Waterproof.Libs.Analysis.ContinuityDomainNat]
Rabs_n_min_m [lemma, in Waterproof.Libs.Analysis.ContinuityDomainNat]
Reals [library]
Reals [library]
reformulate_step_prop_index [lemma, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
reformulate_final_prop_index [lemma, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
reformulate_base_prop_index [lemma, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
reformulate_final_prop_strong [lemma, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
reformulate_base_prop_strong [lemma, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
relation_shift [lemma, in Waterproof.Libs.Analysis.SequencesMetric]
rel1:80 [binder, in Waterproof.Chains.Inequalities]
rel1:83 [binder, in Waterproof.Chains.Inequalities]
rel2:81 [binder, in Waterproof.Chains.Inequalities]
rel2:84 [binder, in Waterproof.Chains.Inequalities]
rel:124 [binder, in Waterproof.Chains.Inequalities]
rel:128 [binder, in Waterproof.Chains.Inequalities]
rel:132 [binder, in Waterproof.Chains.Inequalities]
rel:136 [binder, in Waterproof.Chains.Inequalities]
rel:67 [binder, in Waterproof.Chains.Inequalities]
rel:84 [binder, in Waterproof.Libs.Analysis.Subsequences]
rel:89 [binder, in Waterproof.Libs.Analysis.Subsequences]
Req_false [lemma, in Waterproof.Libs.Reals]
Req_true [lemma, in Waterproof.Libs.Reals]
Rge_lt_or_eq_dec [lemma, in Waterproof.Libs.Reals]
Rge_le_dec [lemma, in Waterproof.Libs.Reals]
Rge_min_abs [lemma, in Waterproof.Libs.Reals]
right [constructor, in Waterproof.Tactics.Either]
right_in_open_closed [lemma, in Waterproof.Libs.Reals]
Rle_ge_dec [lemma, in Waterproof.Libs.Reals]
Rle_abs_min [lemma, in Waterproof.Libs.Reals]
Rlt_ge_dec [lemma, in Waterproof.Libs.Reals]
Rmax_abs [lemma, in Waterproof.Libs.Reals]
R_complete [lemma, in Waterproof.Libs.Analysis.SupAndInf]
r1:11 [binder, in Waterproof.Libs.Reals]
r1:14 [binder, in Waterproof.Libs.Reals]
r1:22 [binder, in Waterproof.Libs.Reals]
r1:24 [binder, in Waterproof.Libs.Reals]
r1:26 [binder, in Waterproof.Libs.Reals]
r1:28 [binder, in Waterproof.Libs.Reals]
r1:9 [binder, in Waterproof.Libs.Reals]
r2:10 [binder, in Waterproof.Libs.Reals]
r2:12 [binder, in Waterproof.Libs.Reals]
r2:15 [binder, in Waterproof.Libs.Reals]
r2:23 [binder, in Waterproof.Libs.Reals]
r2:25 [binder, in Waterproof.Libs.Reals]
r2:27 [binder, in Waterproof.Libs.Reals]
r2:29 [binder, in Waterproof.Libs.Reals]
R:10 [binder, in Waterproof.Libs.Logic.ConstructiveLogic]
R:13 [binder, in Waterproof.Libs.Logic.ConstructiveLogic]
r:13 [binder, in Waterproof.Libs.Reals]
R:16 [binder, in Waterproof.Libs.Logic.ConstructiveLogic]
r:16 [binder, in Waterproof.Libs.Analysis.ContinuityDomainR]
R:19 [binder, in Waterproof.Libs.Logic.ConstructiveLogic]
r:2 [binder, in Waterproof.Libs.Analysis.OpenAndClosed]
R:22 [binder, in Waterproof.Libs.Logic.ConstructiveLogic]
r:6 [binder, in Waterproof.Libs.Analysis.OpenAndClosed]
R:7 [binder, in Waterproof.Libs.Logic.ConstructiveLogic]

S

Sequences [library]
SequencesMetric [library]
sequence_ub_bds [lemma, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
SequentialAccumulationPoints [library]
seq_bdd_seq_acc_pts_bdd [lemma, in Waterproof.Libs.Analysis.SequentialAccumulationPoints]
seq_of_max_is_increasing [lemma, in Waterproof.Libs.Analysis.Subsequences]
seq_of_max [definition, in Waterproof.Libs.Analysis.Subsequences]
seq_ordered_lim_ordered [lemma, in Waterproof.Libs.Analysis.Sequences]
seq_ex_almost_maximizer_m [lemma, in Waterproof.Libs.Analysis.SupAndInf]
seq_ex_almost_maximizer_ε [lemma, in Waterproof.Libs.Analysis.SupAndInf]
seq:13 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
seq:25 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
seq:28 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
seq:35 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
seq:39 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
seq:43 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
seq:58 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
seq:60 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
seq:63 [binder, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
Series [library]
series_cv_abs_to [definition, in Waterproof.Libs.Analysis.Series]
series_cv_abs [definition, in Waterproof.Libs.Analysis.Series]
series_cv [definition, in Waterproof.Libs.Analysis.Series]
series_cv_to [definition, in Waterproof.Libs.Analysis.Series]
Sets [library]
set_opp [definition, in Waterproof.Libs.Analysis.SupAndInf]
sigma_split_v2 [lemma, in Waterproof.Libs.Analysis.Series]
Since [library]
snd_map [definition, in Waterproof.Chains.Inequalities]
Sn_eq_nplus1 [lemma, in Waterproof.Tactics.Induction]
Specialize [library]
squeeze_theorem [lemma, in Waterproof.Libs.Analysis.Sequences]
StateGoal [module, in Waterproof.Util.Goals]
StateGoal.unwrap [definition, in Waterproof.Util.Goals]
StateGoal.wrap [constructor, in Waterproof.Util.Goals]
StateGoal.Wrapper [inductive, in Waterproof.Util.Goals]
StateHyp [module, in Waterproof.Util.Goals]
StateHyp.unwrap [definition, in Waterproof.Util.Goals]
StateHyp.wrap [constructor, in Waterproof.Util.Goals]
StateHyp.Wrapper [inductive, in Waterproof.Util.Goals]
StrongIndIndxSeq [module, in Waterproof.Util.Goals]
StrongIndIndxSeq.unwrap [definition, in Waterproof.Util.Goals]
StrongIndIndxSeq.wrap [constructor, in Waterproof.Util.Goals]
StrongIndIndxSeq.Wrapper [inductive, in Waterproof.Util.Goals]
StrongInduction [section, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
StrongInductionIndexSequence [section, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
StrongInductionIndexSequence [library]
strong_ind_index_seq_with_prop [lemma, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
strong_ind_seq_with_prop [lemma, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
Subsequences [library]
SubsequencesMetric [library]
subsequence_of_convergent_sequence [lemma, in Waterproof.Libs.Analysis.SubsequencesMetric]
subseq_sat_rel [lemma, in Waterproof.Libs.Analysis.Subsequences]
subset [record, in Waterproof.Notations.Sets]
sumbool_comm [lemma, in Waterproof.Tactics.Either]
sumtriad [inductive, in Waterproof.Tactics.Either]
SupAndInf [library]
sup_is_upp_bd [lemma, in Waterproof.Libs.Analysis.SupAndInf]
sup_set_opp_is_inf_set [lemma, in Waterproof.Libs.Analysis.SupAndInf]

T

Tactics [library]
Take [library]
ToShow [library]
total_statement [projection, in Waterproof.Chains.Inequalities]
true_Req [lemma, in Waterproof.Libs.Reals]
TypeCorrector [library]
type_of_test_aux [definition, in Waterproof.Util.Assertions]
type_of [definition, in Waterproof.Util.Init]
T:1 [binder, in Waterproof.Util.Assertions]
T:1 [binder, in Waterproof.Util.Init]
T:10 [binder, in Waterproof.Chains.Inequalities]
T:101 [binder, in Waterproof.Chains.Inequalities]
T:104 [binder, in Waterproof.Chains.Inequalities]
T:109 [binder, in Waterproof.Chains.Inequalities]
T:111 [binder, in Waterproof.Chains.Inequalities]
T:114 [binder, in Waterproof.Chains.Inequalities]
T:117 [binder, in Waterproof.Chains.Inequalities]
T:122 [binder, in Waterproof.Chains.Inequalities]
T:13 [binder, in Waterproof.Chains.Inequalities]
T:21 [binder, in Waterproof.Chains.Inequalities]
T:22 [binder, in Waterproof.Chains.Inequalities]
T:23 [binder, in Waterproof.Chains.Inequalities]
T:24 [binder, in Waterproof.Chains.Inequalities]
T:25 [binder, in Waterproof.Chains.Inequalities]
T:26 [binder, in Waterproof.Chains.Inequalities]
T:27 [binder, in Waterproof.Chains.Inequalities]
T:33 [binder, in Waterproof.Chains.Inequalities]
T:34 [binder, in Waterproof.Chains.Inequalities]
T:35 [binder, in Waterproof.Chains.Inequalities]
T:36 [binder, in Waterproof.Chains.Inequalities]
T:40 [binder, in Waterproof.Chains.Inequalities]
T:44 [binder, in Waterproof.Chains.Inequalities]
T:48 [binder, in Waterproof.Chains.Inequalities]
T:51 [binder, in Waterproof.Chains.Inequalities]
T:54 [binder, in Waterproof.Chains.Inequalities]
T:57 [binder, in Waterproof.Chains.Inequalities]
T:63 [binder, in Waterproof.Chains.Inequalities]
T:66 [binder, in Waterproof.Chains.Inequalities]
T:7 [binder, in Waterproof.Chains.Inequalities]
T:70 [binder, in Waterproof.Chains.Inequalities]
T:73 [binder, in Waterproof.Chains.Inequalities]
T:78 [binder, in Waterproof.Chains.Inequalities]
T:86 [binder, in Waterproof.Chains.Inequalities]
T:90 [binder, in Waterproof.Chains.Inequalities]
T:94 [binder, in Waterproof.Chains.Inequalities]
T:98 [binder, in Waterproof.Chains.Inequalities]

U

Unfold [library]
upp_bd_seq_is_upp_bd_lim [lemma, in Waterproof.Libs.Analysis.Sequences]
upp_bd_set_opp_to_low_bd_set [lemma, in Waterproof.Libs.Analysis.SupAndInf]
upp_bd_set_to_low_bd_set_opp [lemma, in Waterproof.Libs.Analysis.SupAndInf]
U:4 [binder, in Waterproof.Notations.Sets]
U:5 [binder, in Waterproof.Notations.Sets]

V

Version [library]
v:1 [binder, in Waterproof.Tactics.Help]
v:2 [binder, in Waterproof.Tactics.Help]

W

Waterproof [library]
Waterprove [library]
weak_global_statement [projection, in Waterproof.Chains.Inequalities]

X

x0:17 [binder, in Waterproof.Libs.Analysis.SequentialAccumulationPoints]
x0:18 [binder, in Waterproof.Libs.Analysis.SequentialAccumulationPoints]
x:1 [binder, in Waterproof.Util.Constr]
X:1 [binder, in Waterproof.Notations.Sets]
x:1 [binder, in Waterproof.Libs.Reals]
x:1 [binder, in Waterproof.Notations.Common]
X:1 [binder, in Waterproof.Libs.Analysis.MetricSpaces]
x:11 [binder, in Waterproof.Libs.Analysis.OpenAndClosed]
x:11 [binder, in Waterproof.Libs.Analysis.MetricSpaces]
X:12 [binder, in Waterproof.Libs.Analysis.SequencesMetric]
x:12 [binder, in Waterproof.Libs.Analysis.ContinuityDomainR]
x:12 [binder, in Waterproof.Libs.Analysis.MetricSpaces]
x:125 [binder, in Waterproof.Chains.Inequalities]
x:129 [binder, in Waterproof.Chains.Inequalities]
x:13 [binder, in Waterproof.Util.Goals]
x:133 [binder, in Waterproof.Chains.Inequalities]
x:137 [binder, in Waterproof.Chains.Inequalities]
x:14 [binder, in Waterproof.Libs.Analysis.OpenAndClosed]
x:14 [binder, in Waterproof.Libs.Analysis.MetricSpaces]
x:16 [binder, in Waterproof.Libs.Negation]
x:16 [binder, in Waterproof.Libs.Reals]
x:16 [binder, in Waterproof.Libs.Analysis.OpenAndClosed]
x:16 [binder, in Waterproof.Libs.Analysis.MetricSpaces]
x:165 [binder, in Waterproof.Chains.Inequalities]
x:17 [binder, in Waterproof.Libs.Negation]
x:17 [binder, in Waterproof.Libs.Reals]
x:17 [binder, in Waterproof.Libs.Analysis.ContinuityDomainR]
x:17 [binder, in Waterproof.Libs.Analysis.SupAndInf]
x:173 [binder, in Waterproof.Chains.Inequalities]
x:18 [binder, in Waterproof.Libs.Negation]
x:180 [binder, in Waterproof.Chains.Inequalities]
x:189 [binder, in Waterproof.Chains.Inequalities]
x:19 [binder, in Waterproof.Util.Goals]
x:196 [binder, in Waterproof.Chains.Inequalities]
x:2 [binder, in Waterproof.Util.Assertions]
x:2 [binder, in Waterproof.Libs.Analysis.SequentialAccumulationPoints]
x:2 [binder, in Waterproof.Libs.Analysis.SupAndInf]
x:2 [binder, in Waterproof.Util.Init]
x:2 [binder, in Waterproof.Libs.Analysis.MetricSpaces]
x:205 [binder, in Waterproof.Chains.Inequalities]
x:213 [binder, in Waterproof.Chains.Inequalities]
x:22 [binder, in Waterproof.Libs.Negation]
x:22 [binder, in Waterproof.Libs.Analysis.ContinuityDomainR]
x:220 [binder, in Waterproof.Chains.Inequalities]
x:229 [binder, in Waterproof.Chains.Inequalities]
x:23 [binder, in Waterproof.Libs.Negation]
x:236 [binder, in Waterproof.Chains.Inequalities]
x:24 [binder, in Waterproof.Libs.Negation]
x:25 [binder, in Waterproof.Util.Goals]
x:25 [binder, in Waterproof.Libs.Analysis.ContinuityDomainR]
x:27 [binder, in Waterproof.Libs.Analysis.ContinuityDomainR]
x:28 [binder, in Waterproof.Libs.Analysis.ContinuityDomainR]
x:3 [binder, in Waterproof.Libs.Analysis.Sequences]
x:3 [binder, in Waterproof.Libs.Reals]
x:3 [binder, in Waterproof.Libs.Analysis.OpenAndClosed]
x:3 [binder, in Waterproof.Libs.Analysis.ContinuityDomainR]
x:3 [binder, in Waterproof.Notations.Common]
x:30 [binder, in Waterproof.Libs.Analysis.ContinuityDomainR]
x:32 [binder, in Waterproof.Libs.Analysis.ContinuityDomainNat]
x:33 [binder, in Waterproof.Libs.Analysis.ContinuityDomainR]
x:35 [binder, in Waterproof.Util.Goals]
x:35 [binder, in Waterproof.Libs.Analysis.ContinuityDomainNat]
x:36 [binder, in Waterproof.Libs.Analysis.ContinuityDomainR]
x:36 [binder, in Waterproof.Libs.Analysis.ContinuityDomainNat]
x:39 [binder, in Waterproof.Libs.Analysis.ContinuityDomainNat]
x:4 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
x:4 [binder, in Waterproof.Libs.Analysis.MetricSpaces]
x:40 [binder, in Waterproof.Libs.Analysis.SubsequencesMetric]
x:40 [binder, in Waterproof.Libs.Analysis.SupAndInf]
x:42 [binder, in Waterproof.Libs.Analysis.ContinuityDomainNat]
x:43 [binder, in Waterproof.Util.Goals]
x:44 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
x:45 [binder, in Waterproof.Libs.Analysis.SupAndInf]
x:49 [binder, in Waterproof.Util.Goals]
x:5 [binder, in Waterproof.Libs.Reals]
x:5 [binder, in Waterproof.Notations.Common]
x:56 [binder, in Waterproof.Libs.Negation]
x:57 [binder, in Waterproof.Libs.Negation]
x:58 [binder, in Waterproof.Libs.Negation]
x:6 [binder, in Waterproof.Notations.Reals]
x:6 [binder, in Waterproof.Notations.Sets]
x:6 [binder, in Waterproof.Libs.Analysis.ContinuityDomainR]
x:6 [binder, in Waterproof.Libs.Analysis.SupAndInf]
x:6 [binder, in Waterproof.Libs.Analysis.MetricSpaces]
x:62 [binder, in Waterproof.Libs.Negation]
x:63 [binder, in Waterproof.Libs.Negation]
x:64 [binder, in Waterproof.Libs.Negation]
x:68 [binder, in Waterproof.Libs.Negation]
x:68 [binder, in Waterproof.Chains.Inequalities]
x:69 [binder, in Waterproof.Libs.Negation]
x:7 [binder, in Waterproof.Util.Goals]
x:7 [binder, in Waterproof.Notations.Reals]
X:7 [binder, in Waterproof.Libs.Analysis.SequencesMetric]
x:7 [binder, in Waterproof.Libs.Reals]
x:7 [binder, in Waterproof.Libs.Analysis.OpenAndClosed]
x:7 [binder, in Waterproof.Notations.Common]
x:70 [binder, in Waterproof.Libs.Negation]
x:70 [binder, in Waterproof.Libs.Analysis.SupAndInf]
x:74 [binder, in Waterproof.Libs.Negation]
x:75 [binder, in Waterproof.Libs.Negation]
x:76 [binder, in Waterproof.Libs.Negation]
x:76 [binder, in Waterproof.Libs.Analysis.SupAndInf]
x:8 [binder, in Waterproof.Notations.Reals]
x:8 [binder, in Waterproof.Libs.Analysis.SequentialAccumulationPoints]
x:8 [binder, in Waterproof.Libs.Analysis.MetricSpaces]
x:81 [binder, in Waterproof.Libs.Negation]
x:82 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
x:82 [binder, in Waterproof.Libs.Negation]
x:83 [binder, in Waterproof.Libs.Negation]
x:84 [binder, in Waterproof.Libs.Negation]
x:85 [binder, in Waterproof.Libs.Negation]
x:86 [binder, in Waterproof.Libs.Negation]
x:87 [binder, in Waterproof.Libs.Negation]
x:88 [binder, in Waterproof.Libs.Negation]
x:89 [binder, in Waterproof.Libs.Negation]
x:9 [binder, in Waterproof.Notations.Reals]
x:9 [binder, in Waterproof.Notations.Common]
x:90 [binder, in Waterproof.Libs.Negation]
x:91 [binder, in Waterproof.Libs.Negation]
x:92 [binder, in Waterproof.Libs.Negation]
x:94 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
x:97 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
x:98 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]

Y

y_seq [definition, in Waterproof.Libs.Analysis.Sequences]
y:10 [binder, in Waterproof.Notations.Common]
y:126 [binder, in Waterproof.Chains.Inequalities]
y:13 [binder, in Waterproof.Libs.Analysis.MetricSpaces]
y:130 [binder, in Waterproof.Chains.Inequalities]
y:134 [binder, in Waterproof.Chains.Inequalities]
y:138 [binder, in Waterproof.Chains.Inequalities]
y:15 [binder, in Waterproof.Libs.Analysis.MetricSpaces]
y:17 [binder, in Waterproof.Libs.Analysis.MetricSpaces]
y:180 [binder, in Waterproof.Libs.Analysis.SupAndInf]
y:2 [binder, in Waterproof.Libs.Reals]
y:2 [binder, in Waterproof.Notations.Common]
y:27 [binder, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
y:3 [binder, in Waterproof.Libs.Analysis.MetricSpaces]
y:4 [binder, in Waterproof.Libs.Reals]
y:4 [binder, in Waterproof.Notations.Common]
y:41 [binder, in Waterproof.Libs.Analysis.SubsequencesMetric]
y:5 [binder, in Waterproof.Libs.Analysis.MetricSpaces]
y:6 [binder, in Waterproof.Libs.Reals]
y:6 [binder, in Waterproof.Notations.Common]
y:69 [binder, in Waterproof.Chains.Inequalities]
y:7 [binder, in Waterproof.Libs.Analysis.MetricSpaces]
y:8 [binder, in Waterproof.Libs.Reals]
y:8 [binder, in Waterproof.Notations.Common]
y:9 [binder, in Waterproof.Libs.Analysis.MetricSpaces]

Z

zero_in_interval_closed_zero_open_one [lemma, in Waterproof.Libs.Analysis.OpenAndClosed]
z:10 [binder, in Waterproof.Libs.Analysis.MetricSpaces]
z:162 [binder, in Waterproof.Chains.Inequalities]
z:47 [binder, in Waterproof.Libs.Analysis.SupAndInf]

_

_and_assoc1 [lemma, in Waterproof.Waterprove]

other

≥ _ (chain_scope) [notation, in Waterproof.Chains.Inequalities]
>= _ (chain_scope) [notation, in Waterproof.Chains.Inequalities]
> _ (chain_scope) [notation, in Waterproof.Chains.Inequalities]
= _ (chain_scope) [notation, in Waterproof.Chains.Inequalities]
≤ _ (chain_scope) [notation, in Waterproof.Chains.Inequalities]
<= _ (chain_scope) [notation, in Waterproof.Chains.Inequalities]
< _ (chain_scope) [notation, in Waterproof.Chains.Inequalities]
_ is an accumulation point of _ (metric_scope) [notation, in Waterproof.Libs.Analysis.SubsequencesMetric]
_ is an _accumulation point_ of _ (metric_scope) [notation, in Waterproof.Libs.Analysis.SubsequencesMetric]
_ is a subsequence of _ (metric_scope) [notation, in Waterproof.Libs.Analysis.SubsequencesMetric]
_ is a _subsequence_ of _ (metric_scope) [notation, in Waterproof.Libs.Analysis.SubsequencesMetric]
_ is an index sequence (metric_scope) [notation, in Waterproof.Libs.Analysis.SubsequencesMetric]
_ is an _index sequence_ (metric_scope) [notation, in Waterproof.Libs.Analysis.SubsequencesMetric]
_ converges to _ (metric_scope) [notation, in Waterproof.Libs.Analysis.SequencesMetric]
_ _converges to_ _ (metric_scope) [notation, in Waterproof.Libs.Analysis.SequencesMetric]
_ ⟶ _ (metric_scope) [notation, in Waterproof.Libs.Analysis.SequencesMetric]
_ ≥ _ (nat_scope) [notation, in Waterproof.Notations.Reals]
_ ≤ _ (nat_scope) [notation, in Waterproof.Notations.Reals]
( _ , _ ) (R_scope) [notation, in Waterproof.Notations.Reals]
( _ , _ ] (R_scope) [notation, in Waterproof.Notations.Reals]
[ _ , _ ) (R_scope) [notation, in Waterproof.Notations.Reals]
[ _ , _ ] (R_scope) [notation, in Waterproof.Notations.Reals]
｜ _ - _ ｜ (R_scope) [notation, in Waterproof.Notations.Reals]
_ ≥ _ (R_scope) [notation, in Waterproof.Notations.Reals]
_ ≤ _ (R_scope) [notation, in Waterproof.Notations.Reals]
_ : _ (subset_scope) [notation, in Waterproof.Notations.Sets]
_ ≠ _ (type_scope) [notation, in Waterproof.Notations.Reals]
¬ _ (type_scope) [notation, in Waterproof.Notations.Common]
_ ⇔ _ (type_scope) [notation, in Waterproof.Notations.Common]
_ ↔ _ (type_scope) [notation, in Waterproof.Notations.Common]
_ ⇨ _ (type_scope) [notation, in Waterproof.Notations.Common]
_ ⇒ _ (type_scope) [notation, in Waterproof.Notations.Common]
_ → _ (type_scope) [notation, in Waterproof.Notations.Common]
_ ∧ _ (type_scope) [notation, in Waterproof.Notations.Common]
_ ∨ _ (type_scope) [notation, in Waterproof.Notations.Common]
fun _ .. _ ↦ _ (type_scope) [notation, in Waterproof.Notations.Common]
∃ _ .. _ , _ (type_scope) [notation, in Waterproof.Notations.Common]
there exists _ .. _ , _ (type_scope) [notation, in Waterproof.Notations.Common]
∀ _ .. _ , _ (type_scope) [notation, in Waterproof.Notations.Common]
for all _ .. _ , _ (type_scope) [notation, in Waterproof.Notations.Common]
_ ( _ , .. , _ ) (type_scope) [notation, in Waterproof.Notations.Common]
_ ⟶ _ [notation, in Waterproof.Notations.Reals]
_ and _ are disjoint [notation, in Waterproof.Notations.Sets]
_ ⊂ _ [notation, in Waterproof.Notations.Sets]
_ ∉ _ [notation, in Waterproof.Notations.Sets]
_ ∈ _ [notation, in Waterproof.Notations.Sets]
_ \ _ [notation, in Waterproof.Notations.Sets]
_ ∪ _ [notation, in Waterproof.Notations.Sets]
_ ∩ _ [notation, in Waterproof.Notations.Sets]
_ ◦ _ ◦ _ [notation, in Waterproof.Libs.Analysis.SubsequencesMetric]
_ ◦ _ [notation, in Waterproof.Libs.Analysis.SubsequencesMetric]
_ diverges to -∞ [notation, in Waterproof.Libs.Analysis.Sequences]
_ _diverges to -∞_ [notation, in Waterproof.Libs.Analysis.Sequences]
_ ⟶ -∞ [notation, in Waterproof.Libs.Analysis.Sequences]
_ diverges to ∞ [notation, in Waterproof.Libs.Analysis.Sequences]
_ _diverges to ∞_ [notation, in Waterproof.Libs.Analysis.Sequences]
_ ⟶ ∞ [notation, in Waterproof.Libs.Analysis.Sequences]
_ is bounded below [notation, in Waterproof.Libs.Analysis.Sequences]
_ is _bounded below_ [notation, in Waterproof.Libs.Analysis.Sequences]
_ is bounded above [notation, in Waterproof.Libs.Analysis.Sequences]
_ is _bounded above_ [notation, in Waterproof.Libs.Analysis.Sequences]
_ is bounded [notation, in Waterproof.Libs.Analysis.Sequences]
_ is _bounded_ [notation, in Waterproof.Libs.Analysis.Sequences]
_ is closed [notation, in Waterproof.Libs.Analysis.OpenAndClosed]
_ is _closed_ [notation, in Waterproof.Libs.Analysis.OpenAndClosed]
_ is open [notation, in Waterproof.Libs.Analysis.OpenAndClosed]
_ is _open_ [notation, in Waterproof.Libs.Analysis.OpenAndClosed]
_ is an interior point of _ [notation, in Waterproof.Libs.Analysis.OpenAndClosed]
_ is an _interior point_ of _ [notation, in Waterproof.Libs.Analysis.OpenAndClosed]
_ is continuous in _ [notation, in Waterproof.Libs.Analysis.ContinuityDomainR]
_ is _continuous_ in _ [notation, in Waterproof.Libs.Analysis.ContinuityDomainR]
_ is an isolated point [notation, in Waterproof.Libs.Analysis.ContinuityDomainR]
_ is an _isolated point_ [notation, in Waterproof.Libs.Analysis.ContinuityDomainR]
_ is an accumulation point [notation, in Waterproof.Libs.Analysis.ContinuityDomainR]
_ is an _accumulation point_ [notation, in Waterproof.Libs.Analysis.ContinuityDomainR]
_ is a lower bound for _ [notation, in Waterproof.Libs.Analysis.SupAndInf]
_ is a _lower bound_ for _ [notation, in Waterproof.Libs.Analysis.SupAndInf]
_ is bounded from below [notation, in Waterproof.Libs.Analysis.SupAndInf]
_ is _bounded from below_ [notation, in Waterproof.Libs.Analysis.SupAndInf]
_ is the infimum of _ [notation, in Waterproof.Libs.Analysis.SupAndInf]
_ is the _infimum_ of _ [notation, in Waterproof.Libs.Analysis.SupAndInf]
_ is the maximum of _ [notation, in Waterproof.Libs.Analysis.SupAndInf]
_ is the _maximum_ of _ [notation, in Waterproof.Libs.Analysis.SupAndInf]
_ is an upper bound for _ [notation, in Waterproof.Libs.Analysis.SupAndInf]
_ is an _upper bound_ for _ [notation, in Waterproof.Libs.Analysis.SupAndInf]
_ is bounded from above [notation, in Waterproof.Libs.Analysis.SupAndInf]
_ is _bounded from above_ [notation, in Waterproof.Libs.Analysis.SupAndInf]
_ is the supremum of _ [notation, in Waterproof.Libs.Analysis.SupAndInf]
_ is the _supremum_ of _ [notation, in Waterproof.Libs.Analysis.SupAndInf]
_ is continuous in _ [notation, in Waterproof.Libs.Analysis.ContinuityDomainNat]
_ is _continuous_ in _ [notation, in Waterproof.Libs.Analysis.ContinuityDomainNat]
_ is an isolated point [notation, in Waterproof.Libs.Analysis.ContinuityDomainNat]
_ is an _isolated point_ [notation, in Waterproof.Libs.Analysis.ContinuityDomainNat]
_ is an accumulation point [notation, in Waterproof.Libs.Analysis.ContinuityDomainNat]
_ is an _accumulation point_ [notation, in Waterproof.Libs.Analysis.ContinuityDomainNat]
Add the following line to the proof: Take k : ℕ and assume n(0),...,n(k) are defined. [notation, in Waterproof.Util.Goals]
Add the following line to the proof: Assume that ( _ ). [notation, in Waterproof.Util.Goals]
Add the following line to the proof: It holds that ( _ ). [notation, in Waterproof.Util.Goals]
Add the following line to the proof: We need to show that ( _ ). or write: We conclude that ( _ ). if no intermediary proof steps are required. [notation, in Waterproof.Util.Goals]
Add the following line to the proof: We now show the induction step. [notation, in Waterproof.Util.Goals]
Add the following line to the proof: We first show the base case ( _ ). [notation, in Waterproof.Util.Goals]
Add the following line to the proof: Case ( _ ). [notation, in Waterproof.Util.Goals]
B( _ , _ ) [notation, in Waterproof.Libs.Analysis.OpenAndClosed]
Derive a contradiction. [notation, in Waterproof.Notations.Common]
limit of _ in _ is _ [notation, in Waterproof.Libs.Analysis.ContinuityDomainR]
limit of _ in _ is _ [notation, in Waterproof.Libs.Analysis.ContinuityDomainNat]
set_of_subsets _ [notation, in Waterproof.Notations.Sets]
_limit_ of _ in _ is _ [notation, in Waterproof.Libs.Analysis.ContinuityDomainR]
_limit_ of _ in _ is _ [notation, in Waterproof.Libs.Analysis.ContinuityDomainNat]
& _ _ _ .. _ [notation, in Waterproof.Chains.Inequalities]
| _ | [notation, in Waterproof.Notations.Reals]
Σ _ equals _ [notation, in Waterproof.Notations.Reals]
Ω [notation, in Waterproof.Notations.Sets]
ℕ [notation, in Waterproof.Notations.Reals]
ℚ [notation, in Waterproof.Notations.Reals]
ℝ [notation, in Waterproof.Notations.Reals]
ℝ \ _ [notation, in Waterproof.Libs.Analysis.OpenAndClosed]
ℝ\ _ [notation, in Waterproof.Libs.Analysis.OpenAndClosed]
ℤ [notation, in Waterproof.Notations.Reals]
∅ [notation, in Waterproof.Notations.Sets]
｛ _ : _ | _ ｝ [notation, in Waterproof.Notations.Sets]
δ1:26 [binder, in Waterproof.Libs.Analysis.ContinuityDomainR]
δ:11 [binder, in Waterproof.Libs.Analysis.ContinuityDomainR]
δ:21 [binder, in Waterproof.Libs.Analysis.ContinuityDomainR]
δ:24 [binder, in Waterproof.Libs.Analysis.ContinuityDomainR]
δ:24 [binder, in Waterproof.Libs.Analysis.ContinuityDomainNat]
δ:31 [binder, in Waterproof.Libs.Analysis.ContinuityDomainNat]
δ:32 [binder, in Waterproof.Libs.Analysis.ContinuityDomainR]
δ:34 [binder, in Waterproof.Libs.Analysis.ContinuityDomainNat]
δ:35 [binder, in Waterproof.Libs.Analysis.ContinuityDomainR]
δ:38 [binder, in Waterproof.Libs.Analysis.ContinuityDomainNat]
δ:41 [binder, in Waterproof.Libs.Analysis.ContinuityDomainNat]
ε:10 [binder, in Waterproof.Libs.Analysis.ContinuityDomainR]
ε:100 [binder, in Waterproof.Libs.Analysis.SupAndInf]
ε:105 [binder, in Waterproof.Libs.Analysis.SupAndInf]
ε:108 [binder, in Waterproof.Libs.Analysis.SupAndInf]
ε:113 [binder, in Waterproof.Libs.Analysis.SupAndInf]
ε:117 [binder, in Waterproof.Libs.Analysis.SupAndInf]
ε:121 [binder, in Waterproof.Libs.Analysis.SupAndInf]
ε:125 [binder, in Waterproof.Libs.Analysis.SupAndInf]
ε:129 [binder, in Waterproof.Libs.Analysis.SupAndInf]
ε:13 [binder, in Waterproof.Libs.Analysis.Sequences]
ε:133 [binder, in Waterproof.Libs.Analysis.SupAndInf]
ε:135 [binder, in Waterproof.Libs.Analysis.SupAndInf]
ε:137 [binder, in Waterproof.Libs.Analysis.SupAndInf]
ε:141 [binder, in Waterproof.Libs.Analysis.SupAndInf]
ε:145 [binder, in Waterproof.Libs.Analysis.SupAndInf]
ε:149 [binder, in Waterproof.Libs.Analysis.SupAndInf]
ε:15 [binder, in Waterproof.Libs.Analysis.ContinuityDomainNat]
ε:151 [binder, in Waterproof.Libs.Analysis.SupAndInf]
ε:153 [binder, in Waterproof.Libs.Analysis.SupAndInf]
ε:155 [binder, in Waterproof.Libs.Analysis.SupAndInf]
ε:175 [binder, in Waterproof.Libs.Analysis.SupAndInf]
ε:177 [binder, in Waterproof.Libs.Analysis.SupAndInf]
ε:18 [binder, in Waterproof.Libs.Analysis.ContinuityDomainNat]
ε:2 [binder, in Waterproof.Libs.Analysis.ContinuityDomainR]
ε:20 [binder, in Waterproof.Libs.Analysis.ContinuityDomainR]
ε:23 [binder, in Waterproof.Libs.Analysis.ContinuityDomainR]
ε:23 [binder, in Waterproof.Libs.Analysis.ContinuityDomainNat]
ε:29 [binder, in Waterproof.Libs.Analysis.ContinuityDomainR]
ε:3 [binder, in Waterproof.Notations.Reals]
ε:30 [binder, in Waterproof.Libs.Analysis.Sequences]
ε:30 [binder, in Waterproof.Libs.Analysis.ContinuityDomainNat]
ε:31 [binder, in Waterproof.Libs.Analysis.ContinuityDomainR]
ε:33 [binder, in Waterproof.Libs.Analysis.ContinuityDomainNat]
ε:34 [binder, in Waterproof.Libs.Analysis.ContinuityDomainR]
ε:35 [binder, in Waterproof.Libs.Analysis.SubsequencesMetric]
ε:35 [binder, in Waterproof.Libs.Analysis.Sequences]
ε:37 [binder, in Waterproof.Libs.Analysis.ContinuityDomainNat]
ε:4 [binder, in Waterproof.Libs.Analysis.SequencesMetric]
ε:40 [binder, in Waterproof.Libs.Analysis.ContinuityDomainNat]
ε:43 [binder, in Waterproof.Libs.Analysis.ContinuityDomainNat]
ε:47 [binder, in Waterproof.Libs.Analysis.SubsequencesMetric]
ε:5 [binder, in Waterproof.Libs.Analysis.ContinuityDomainR]
ε:50 [binder, in Waterproof.Libs.Analysis.Sequences]
ε:97 [binder, in Waterproof.Libs.Analysis.SupAndInf]

Notation Index

other

≥ _ (chain_scope) [in Waterproof.Chains.Inequalities]
>= _ (chain_scope) [in Waterproof.Chains.Inequalities]
> _ (chain_scope) [in Waterproof.Chains.Inequalities]
= _ (chain_scope) [in Waterproof.Chains.Inequalities]
≤ _ (chain_scope) [in Waterproof.Chains.Inequalities]
<= _ (chain_scope) [in Waterproof.Chains.Inequalities]
< _ (chain_scope) [in Waterproof.Chains.Inequalities]
_ is an accumulation point of _ (metric_scope) [in Waterproof.Libs.Analysis.SubsequencesMetric]
_ is an _accumulation point_ of _ (metric_scope) [in Waterproof.Libs.Analysis.SubsequencesMetric]
_ is a subsequence of _ (metric_scope) [in Waterproof.Libs.Analysis.SubsequencesMetric]
_ is a _subsequence_ of _ (metric_scope) [in Waterproof.Libs.Analysis.SubsequencesMetric]
_ is an index sequence (metric_scope) [in Waterproof.Libs.Analysis.SubsequencesMetric]
_ is an _index sequence_ (metric_scope) [in Waterproof.Libs.Analysis.SubsequencesMetric]
_ converges to _ (metric_scope) [in Waterproof.Libs.Analysis.SequencesMetric]
_ _converges to_ _ (metric_scope) [in Waterproof.Libs.Analysis.SequencesMetric]
_ ⟶ _ (metric_scope) [in Waterproof.Libs.Analysis.SequencesMetric]
_ ≥ _ (nat_scope) [in Waterproof.Notations.Reals]
_ ≤ _ (nat_scope) [in Waterproof.Notations.Reals]
( _ , _ ) (R_scope) [in Waterproof.Notations.Reals]
( _ , _ ] (R_scope) [in Waterproof.Notations.Reals]
[ _ , _ ) (R_scope) [in Waterproof.Notations.Reals]
[ _ , _ ] (R_scope) [in Waterproof.Notations.Reals]
｜ _ - _ ｜ (R_scope) [in Waterproof.Notations.Reals]
_ ≥ _ (R_scope) [in Waterproof.Notations.Reals]
_ ≤ _ (R_scope) [in Waterproof.Notations.Reals]
_ : _ (subset_scope) [in Waterproof.Notations.Sets]
_ ≠ _ (type_scope) [in Waterproof.Notations.Reals]
¬ _ (type_scope) [in Waterproof.Notations.Common]
_ ⇔ _ (type_scope) [in Waterproof.Notations.Common]
_ ↔ _ (type_scope) [in Waterproof.Notations.Common]
_ ⇨ _ (type_scope) [in Waterproof.Notations.Common]
_ ⇒ _ (type_scope) [in Waterproof.Notations.Common]
_ → _ (type_scope) [in Waterproof.Notations.Common]
_ ∧ _ (type_scope) [in Waterproof.Notations.Common]
_ ∨ _ (type_scope) [in Waterproof.Notations.Common]
fun _ .. _ ↦ _ (type_scope) [in Waterproof.Notations.Common]
∃ _ .. _ , _ (type_scope) [in Waterproof.Notations.Common]
there exists _ .. _ , _ (type_scope) [in Waterproof.Notations.Common]
∀ _ .. _ , _ (type_scope) [in Waterproof.Notations.Common]
for all _ .. _ , _ (type_scope) [in Waterproof.Notations.Common]
_ ( _ , .. , _ ) (type_scope) [in Waterproof.Notations.Common]
_ ⟶ _ [in Waterproof.Notations.Reals]
_ and _ are disjoint [in Waterproof.Notations.Sets]
_ ⊂ _ [in Waterproof.Notations.Sets]
_ ∉ _ [in Waterproof.Notations.Sets]
_ ∈ _ [in Waterproof.Notations.Sets]
_ \ _ [in Waterproof.Notations.Sets]
_ ∪ _ [in Waterproof.Notations.Sets]
_ ∩ _ [in Waterproof.Notations.Sets]
_ ◦ _ ◦ _ [in Waterproof.Libs.Analysis.SubsequencesMetric]
_ ◦ _ [in Waterproof.Libs.Analysis.SubsequencesMetric]
_ diverges to -∞ [in Waterproof.Libs.Analysis.Sequences]
_ _diverges to -∞_ [in Waterproof.Libs.Analysis.Sequences]
_ ⟶ -∞ [in Waterproof.Libs.Analysis.Sequences]
_ diverges to ∞ [in Waterproof.Libs.Analysis.Sequences]
_ _diverges to ∞_ [in Waterproof.Libs.Analysis.Sequences]
_ ⟶ ∞ [in Waterproof.Libs.Analysis.Sequences]
_ is bounded below [in Waterproof.Libs.Analysis.Sequences]
_ is _bounded below_ [in Waterproof.Libs.Analysis.Sequences]
_ is bounded above [in Waterproof.Libs.Analysis.Sequences]
_ is _bounded above_ [in Waterproof.Libs.Analysis.Sequences]
_ is bounded [in Waterproof.Libs.Analysis.Sequences]
_ is _bounded_ [in Waterproof.Libs.Analysis.Sequences]
_ is closed [in Waterproof.Libs.Analysis.OpenAndClosed]
_ is _closed_ [in Waterproof.Libs.Analysis.OpenAndClosed]
_ is open [in Waterproof.Libs.Analysis.OpenAndClosed]
_ is _open_ [in Waterproof.Libs.Analysis.OpenAndClosed]
_ is an interior point of _ [in Waterproof.Libs.Analysis.OpenAndClosed]
_ is an _interior point_ of _ [in Waterproof.Libs.Analysis.OpenAndClosed]
_ is continuous in _ [in Waterproof.Libs.Analysis.ContinuityDomainR]
_ is _continuous_ in _ [in Waterproof.Libs.Analysis.ContinuityDomainR]
_ is an isolated point [in Waterproof.Libs.Analysis.ContinuityDomainR]
_ is an _isolated point_ [in Waterproof.Libs.Analysis.ContinuityDomainR]
_ is an accumulation point [in Waterproof.Libs.Analysis.ContinuityDomainR]
_ is an _accumulation point_ [in Waterproof.Libs.Analysis.ContinuityDomainR]
_ is a lower bound for _ [in Waterproof.Libs.Analysis.SupAndInf]
_ is a _lower bound_ for _ [in Waterproof.Libs.Analysis.SupAndInf]
_ is bounded from below [in Waterproof.Libs.Analysis.SupAndInf]
_ is _bounded from below_ [in Waterproof.Libs.Analysis.SupAndInf]
_ is the infimum of _ [in Waterproof.Libs.Analysis.SupAndInf]
_ is the _infimum_ of _ [in Waterproof.Libs.Analysis.SupAndInf]
_ is the maximum of _ [in Waterproof.Libs.Analysis.SupAndInf]
_ is the _maximum_ of _ [in Waterproof.Libs.Analysis.SupAndInf]
_ is an upper bound for _ [in Waterproof.Libs.Analysis.SupAndInf]
_ is an _upper bound_ for _ [in Waterproof.Libs.Analysis.SupAndInf]
_ is bounded from above [in Waterproof.Libs.Analysis.SupAndInf]
_ is _bounded from above_ [in Waterproof.Libs.Analysis.SupAndInf]
_ is the supremum of _ [in Waterproof.Libs.Analysis.SupAndInf]
_ is the _supremum_ of _ [in Waterproof.Libs.Analysis.SupAndInf]
_ is continuous in _ [in Waterproof.Libs.Analysis.ContinuityDomainNat]
_ is _continuous_ in _ [in Waterproof.Libs.Analysis.ContinuityDomainNat]
_ is an isolated point [in Waterproof.Libs.Analysis.ContinuityDomainNat]
_ is an _isolated point_ [in Waterproof.Libs.Analysis.ContinuityDomainNat]
_ is an accumulation point [in Waterproof.Libs.Analysis.ContinuityDomainNat]
_ is an _accumulation point_ [in Waterproof.Libs.Analysis.ContinuityDomainNat]
Add the following line to the proof: Take k : ℕ and assume n(0),...,n(k) are defined. [in Waterproof.Util.Goals]
Add the following line to the proof: Assume that ( _ ). [in Waterproof.Util.Goals]
Add the following line to the proof: It holds that ( _ ). [in Waterproof.Util.Goals]
Add the following line to the proof: We need to show that ( _ ). or write: We conclude that ( _ ). if no intermediary proof steps are required. [in Waterproof.Util.Goals]
Add the following line to the proof: We now show the induction step. [in Waterproof.Util.Goals]
Add the following line to the proof: We first show the base case ( _ ). [in Waterproof.Util.Goals]
Add the following line to the proof: Case ( _ ). [in Waterproof.Util.Goals]
B( _ , _ ) [in Waterproof.Libs.Analysis.OpenAndClosed]
Derive a contradiction. [in Waterproof.Notations.Common]
limit of _ in _ is _ [in Waterproof.Libs.Analysis.ContinuityDomainR]
limit of _ in _ is _ [in Waterproof.Libs.Analysis.ContinuityDomainNat]
set_of_subsets _ [in Waterproof.Notations.Sets]
_limit_ of _ in _ is _ [in Waterproof.Libs.Analysis.ContinuityDomainR]
_limit_ of _ in _ is _ [in Waterproof.Libs.Analysis.ContinuityDomainNat]
& _ _ _ .. _ [in Waterproof.Chains.Inequalities]
| _ | [in Waterproof.Notations.Reals]
Σ _ equals _ [in Waterproof.Notations.Reals]
Ω [in Waterproof.Notations.Sets]
ℕ [in Waterproof.Notations.Reals]
ℚ [in Waterproof.Notations.Reals]
ℝ [in Waterproof.Notations.Reals]
ℝ \ _ [in Waterproof.Libs.Analysis.OpenAndClosed]
ℝ\ _ [in Waterproof.Libs.Analysis.OpenAndClosed]
ℤ [in Waterproof.Notations.Reals]
∅ [in Waterproof.Notations.Sets]
｛ _ : _ | _ ｝ [in Waterproof.Notations.Sets]

Binder Index

A

a0:179 [in Waterproof.Libs.Analysis.SupAndInf]
a0:18 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
a0:35 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
a0:50 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
A:1 [in Waterproof.Tactics.Either]
a:1 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
A:1 [in Waterproof.Util.Goals]
a:1 [in Waterproof.Notations.Reals]
A:1 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
A:1 [in Waterproof.Libs.Negation]
a:1 [in Waterproof.Libs.Analysis.SequentialAccumulationPoints]
a:1 [in Waterproof.Libs.Analysis.Subsequences]
a:1 [in Waterproof.Libs.Analysis.Series]
a:1 [in Waterproof.Libs.Analysis.ContinuityDomainR]
A:1 [in Waterproof.Libs.Analysis.SupAndInf]
A:1 [in Waterproof.Waterprove]
A:10 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
a:10 [in Waterproof.Libs.Analysis.Sequences]
A:10 [in Waterproof.Libs.Analysis.OpenAndClosed]
a:10 [in Waterproof.Libs.Analysis.SupAndInf]
a:101 [in Waterproof.Libs.Analysis.SupAndInf]
a:102 [in Waterproof.Libs.Analysis.SupAndInf]
A:103 [in Waterproof.Libs.Analysis.SupAndInf]
a:105 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
a:106 [in Waterproof.Libs.Analysis.SupAndInf]
A:108 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
a:109 [in Waterproof.Libs.Analysis.SupAndInf]
A:11 [in Waterproof.Tactics.Either]
a:11 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
a:11 [in Waterproof.Libs.Analysis.Series]
A:11 [in Waterproof.Libs.Analysis.SupAndInf]
a:110 [in Waterproof.Libs.Analysis.SupAndInf]
A:111 [in Waterproof.Libs.Analysis.SupAndInf]
a:114 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
a:114 [in Waterproof.Libs.Analysis.SupAndInf]
A:115 [in Waterproof.Libs.Analysis.SupAndInf]
a:116 [in Waterproof.Libs.Analysis.Sequences]
a:117 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
a:118 [in Waterproof.Libs.Analysis.SupAndInf]
a:119 [in Waterproof.Libs.Analysis.Sequences]
A:119 [in Waterproof.Libs.Analysis.SupAndInf]
A:12 [in Waterproof.Libs.Analysis.OpenAndClosed]
a:120 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
a:122 [in Waterproof.Libs.Analysis.Sequences]
a:122 [in Waterproof.Libs.Analysis.SupAndInf]
A:123 [in Waterproof.Libs.Analysis.SupAndInf]
a:124 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
a:126 [in Waterproof.Libs.Analysis.Sequences]
a:126 [in Waterproof.Libs.Analysis.SupAndInf]
A:127 [in Waterproof.Libs.Analysis.SupAndInf]
a:129 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
A:13 [in Waterproof.Libs.Negation]
a:13 [in Waterproof.Libs.Analysis.SubsequencesMetric]
a:13 [in Waterproof.Libs.Analysis.SequencesMetric]
a:13 [in Waterproof.Libs.Analysis.Series]
A:13 [in Waterproof.Libs.Analysis.OpenAndClosed]
A:13 [in Waterproof.Libs.Analysis.SupAndInf]
a:130 [in Waterproof.Libs.Analysis.SupAndInf]
a:134 [in Waterproof.Libs.Analysis.SupAndInf]
a:136 [in Waterproof.Libs.Analysis.SupAndInf]
a:138 [in Waterproof.Libs.Analysis.SupAndInf]
A:14 [in Waterproof.Tactics.Either]
a:14 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
a:14 [in Waterproof.Libs.Analysis.ContinuityDomainR]
a:14 [in Waterproof.Libs.Analysis.ContinuityDomainNat]
A:140 [in Waterproof.Chains.Inequalities]
a:142 [in Waterproof.Libs.Analysis.SupAndInf]
A:143 [in Waterproof.Libs.Analysis.SupAndInf]
A:146 [in Waterproof.Chains.Inequalities]
a:146 [in Waterproof.Libs.Analysis.SupAndInf]
A:15 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
a:15 [in Waterproof.Libs.Analysis.Series]
A:15 [in Waterproof.Libs.Analysis.OpenAndClosed]
a:15 [in Waterproof.Libs.Analysis.ContinuityDomainR]
a:150 [in Waterproof.Libs.Analysis.SupAndInf]
A:152 [in Waterproof.Chains.Inequalities]
a:152 [in Waterproof.Libs.Analysis.SupAndInf]
a:154 [in Waterproof.Libs.Analysis.SupAndInf]
a:156 [in Waterproof.Libs.Analysis.SupAndInf]
A:158 [in Waterproof.Chains.Inequalities]
A:16 [in Waterproof.Chains.Inequalities]
A:16 [in Waterproof.Libs.Analysis.SupAndInf]
A:160 [in Waterproof.Libs.Analysis.SupAndInf]
a:162 [in Waterproof.Libs.Analysis.SupAndInf]
a:163 [in Waterproof.Libs.Analysis.SupAndInf]
a:164 [in Waterproof.Libs.Analysis.SupAndInf]
a:165 [in Waterproof.Libs.Analysis.SupAndInf]
a:166 [in Waterproof.Libs.Analysis.SupAndInf]
A:167 [in Waterproof.Libs.Analysis.SupAndInf]
A:17 [in Waterproof.Tactics.Either]
a:17 [in Waterproof.Libs.Analysis.ContinuityDomainNat]
A:170 [in Waterproof.Libs.Analysis.SupAndInf]
a:173 [in Waterproof.Libs.Analysis.SupAndInf]
a:18 [in Waterproof.Libs.Analysis.Series]
a:18 [in Waterproof.Libs.Reals]
A:18 [in Waterproof.Libs.Analysis.SupAndInf]
a:182 [in Waterproof.Libs.Analysis.SupAndInf]
a:186 [in Waterproof.Libs.Analysis.SupAndInf]
A:19 [in Waterproof.Libs.Negation]
a:19 [in Waterproof.Libs.Analysis.ContinuityDomainR]
a:2 [in Waterproof.Libs.Analysis.SequencesMetric]
A:20 [in Waterproof.Tactics.Either]
a:20 [in Waterproof.Libs.Analysis.Sequences]
a:20 [in Waterproof.Libs.Reals]
a:21 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
A:21 [in Waterproof.Libs.Analysis.SupAndInf]
a:21 [in Waterproof.Libs.Analysis.ContinuityDomainNat]
a:22 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
A:23 [in Waterproof.Tactics.Either]
A:24 [in Waterproof.Libs.Analysis.SupAndInf]
A:25 [in Waterproof.Libs.Negation]
a:26 [in Waterproof.Libs.Analysis.SupAndInf]
A:27 [in Waterproof.Util.Goals]
a:27 [in Waterproof.Libs.Analysis.ContinuityDomainNat]
A:28 [in Waterproof.Chains.Inequalities]
A:28 [in Waterproof.Libs.Analysis.SupAndInf]
a:29 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
A:29 [in Waterproof.Libs.Negation]
a:29 [in Waterproof.Libs.Analysis.ContinuityDomainNat]
A:3 [in Waterproof.Tactics.Either]
A:3 [in Waterproof.Libs.Analysis.SupAndInf]
a:30 [in Waterproof.Libs.Reals]
a:30 [in Waterproof.Libs.Analysis.SupAndInf]
A:31 [in Waterproof.Libs.Analysis.SupAndInf]
A:32 [in Waterproof.Util.Goals]
A:32 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
a:32 [in Waterproof.Libs.Analysis.Subsequences]
a:32 [in Waterproof.Libs.Analysis.SubsequencesMetric]
a:32 [in Waterproof.Libs.Reals]
A:33 [in Waterproof.Libs.Negation]
A:34 [in Waterproof.Libs.Analysis.SupAndInf]
A:37 [in Waterproof.Util.Goals]
A:37 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
A:37 [in Waterproof.Libs.Negation]
a:39 [in Waterproof.Libs.Analysis.SupAndInf]
a:4 [in Waterproof.Libs.Analysis.OpenAndClosed]
a:4 [in Waterproof.Libs.Analysis.ContinuityDomainR]
a:4 [in Waterproof.Libs.Analysis.SupAndInf]
a:40 [in Waterproof.Libs.Analysis.Subsequences]
A:41 [in Waterproof.Util.Goals]
A:41 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
A:41 [in Waterproof.Libs.Negation]
A:44 [in Waterproof.Libs.Negation]
a:44 [in Waterproof.Libs.Analysis.Sequences]
A:44 [in Waterproof.Libs.Analysis.SupAndInf]
A:47 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
A:47 [in Waterproof.Libs.Negation]
a:49 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
A:5 [in Waterproof.Util.Goals]
A:5 [in Waterproof.Libs.Negation]
a:5 [in Waterproof.Libs.Analysis.SequentialAccumulationPoints]
a:5 [in Waterproof.Libs.Analysis.Series]
A:5 [in Waterproof.Libs.Analysis.OpenAndClosed]
A:50 [in Waterproof.Libs.Negation]
A:50 [in Waterproof.Libs.Analysis.SupAndInf]
A:53 [in Waterproof.Libs.Negation]
A:54 [in Waterproof.Libs.Analysis.SupAndInf]
a:55 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
a:57 [in Waterproof.Libs.Analysis.Sequences]
A:58 [in Waterproof.Libs.Analysis.SupAndInf]
A:59 [in Waterproof.Libs.Negation]
a:6 [in Waterproof.Libs.Analysis.Sequences]
A:61 [in Waterproof.Libs.Analysis.SupAndInf]
A:65 [in Waterproof.Libs.Negation]
A:65 [in Waterproof.Libs.Analysis.SupAndInf]
a:67 [in Waterproof.Libs.Analysis.Sequences]
a:68 [in Waterproof.Libs.Analysis.SupAndInf]
a:69 [in Waterproof.Libs.Analysis.SupAndInf]
A:7 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
a:71 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
A:71 [in Waterproof.Libs.Negation]
A:71 [in Waterproof.Libs.Analysis.SupAndInf]
a:74 [in Waterproof.Libs.Analysis.Sequences]
a:74 [in Waterproof.Libs.Analysis.SupAndInf]
a:75 [in Waterproof.Libs.Analysis.SupAndInf]
A:77 [in Waterproof.Libs.Negation]
A:77 [in Waterproof.Libs.Analysis.SupAndInf]
A:79 [in Waterproof.Libs.Negation]
A:8 [in Waterproof.Tactics.Either]
a:8 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
a:8 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
a:8 [in Waterproof.Libs.Analysis.SequencesMetric]
A:8 [in Waterproof.Libs.Analysis.OpenAndClosed]
a:8 [in Waterproof.Libs.Analysis.ContinuityDomainR]
A:8 [in Waterproof.Libs.Analysis.SupAndInf]
a:80 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
a:80 [in Waterproof.Libs.Analysis.SupAndInf]
a:83 [in Waterproof.Libs.Analysis.SupAndInf]
a:84 [in Waterproof.Libs.Analysis.SupAndInf]
a:85 [in Waterproof.Libs.Analysis.SupAndInf]
A:86 [in Waterproof.Libs.Analysis.SupAndInf]
a:89 [in Waterproof.Libs.Analysis.SupAndInf]
A:9 [in Waterproof.Libs.Negation]
a:9 [in Waterproof.Libs.Analysis.SubsequencesMetric]
a:9 [in Waterproof.Libs.Analysis.Series]
a:9 [in Waterproof.Libs.Analysis.OpenAndClosed]
a:90 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
a:90 [in Waterproof.Libs.Analysis.Sequences]
a:92 [in Waterproof.Libs.Analysis.Subsequences]
a:92 [in Waterproof.Libs.Analysis.SupAndInf]
a:93 [in Waterproof.Libs.Analysis.SupAndInf]
a:94 [in Waterproof.Libs.Analysis.Sequences]
a:94 [in Waterproof.Libs.Analysis.SupAndInf]
A:95 [in Waterproof.Libs.Analysis.SupAndInf]
a:97 [in Waterproof.Libs.Analysis.Sequences]
a:98 [in Waterproof.Libs.Analysis.SupAndInf]

B

B:10 [in Waterproof.Libs.Negation]
B:109 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
b:11 [in Waterproof.Libs.Analysis.Sequences]
b:115 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
b:118 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
B:12 [in Waterproof.Tactics.Either]
b:121 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
b:126 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
b:131 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
b:134 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
b:138 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
B:141 [in Waterproof.Chains.Inequalities]
B:147 [in Waterproof.Chains.Inequalities]
B:15 [in Waterproof.Tactics.Either]
B:153 [in Waterproof.Chains.Inequalities]
B:159 [in Waterproof.Chains.Inequalities]
b:169 [in Waterproof.Libs.Analysis.SupAndInf]
B:17 [in Waterproof.Chains.Inequalities]
b:172 [in Waterproof.Libs.Analysis.SupAndInf]
B:18 [in Waterproof.Tactics.Either]
b:19 [in Waterproof.Libs.Reals]
B:2 [in Waterproof.Tactics.Either]
B:2 [in Waterproof.Libs.Negation]
B:2 [in Waterproof.Waterprove]
b:20 [in Waterproof.Libs.Analysis.SupAndInf]
B:21 [in Waterproof.Tactics.Either]
b:21 [in Waterproof.Libs.Analysis.Sequences]
b:21 [in Waterproof.Libs.Reals]
b:23 [in Waterproof.Libs.Analysis.SupAndInf]
B:24 [in Waterproof.Tactics.Either]
B:26 [in Waterproof.Libs.Negation]
b:27 [in Waterproof.Libs.Analysis.SupAndInf]
B:29 [in Waterproof.Chains.Inequalities]
B:30 [in Waterproof.Libs.Negation]
b:31 [in Waterproof.Libs.Reals]
b:33 [in Waterproof.Libs.Reals]
B:34 [in Waterproof.Libs.Negation]
B:38 [in Waterproof.Libs.Negation]
b:39 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
B:4 [in Waterproof.Tactics.Either]
b:4 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
b:42 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
B:42 [in Waterproof.Libs.Negation]
b:43 [in Waterproof.Libs.Analysis.SupAndInf]
B:45 [in Waterproof.Libs.Negation]
b:45 [in Waterproof.Libs.Analysis.Sequences]
B:48 [in Waterproof.Libs.Negation]
B:51 [in Waterproof.Libs.Negation]
b:52 [in Waterproof.Libs.Analysis.SupAndInf]
B:6 [in Waterproof.Libs.Negation]
b:7 [in Waterproof.Libs.Analysis.Sequences]
b:75 [in Waterproof.Libs.Analysis.Sequences]
B:78 [in Waterproof.Libs.Negation]
b:8 [in Waterproof.Libs.Analysis.SubsequencesMetric]
B:80 [in Waterproof.Libs.Negation]
B:9 [in Waterproof.Tactics.Either]
b:93 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
b:96 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]

C

C:10 [in Waterproof.Tactics.Either]
c:100 [in Waterproof.Chains.Inequalities]
c:103 [in Waterproof.Chains.Inequalities]
c:106 [in Waterproof.Chains.Inequalities]
C:11 [in Waterproof.Libs.Negation]
C:110 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
c:113 [in Waterproof.Chains.Inequalities]
c:116 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
c:116 [in Waterproof.Chains.Inequalities]
c:119 [in Waterproof.Chains.Inequalities]
C:13 [in Waterproof.Tactics.Either]
c:143 [in Waterproof.Chains.Inequalities]
c:149 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
c:149 [in Waterproof.Chains.Inequalities]
c:151 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
c:155 [in Waterproof.Chains.Inequalities]
C:16 [in Waterproof.Tactics.Either]
C:160 [in Waterproof.Chains.Inequalities]
C:18 [in Waterproof.Chains.Inequalities]
C:19 [in Waterproof.Tactics.Either]
c:2 [in Waterproof.Notations.Reals]
C:22 [in Waterproof.Tactics.Either]
C:25 [in Waterproof.Tactics.Either]
C:27 [in Waterproof.Libs.Negation]
c:27 [in Waterproof.Libs.Analysis.Sequences]
c:29 [in Waterproof.Libs.Analysis.Sequences]
C:3 [in Waterproof.Libs.Negation]
c:3 [in Waterproof.Libs.Analysis.SequencesMetric]
C:3 [in Waterproof.Waterprove]
C:30 [in Waterproof.Chains.Inequalities]
C:31 [in Waterproof.Libs.Negation]
C:35 [in Waterproof.Libs.Negation]
c:37 [in Waterproof.Chains.Inequalities]
C:39 [in Waterproof.Libs.Negation]
c:41 [in Waterproof.Chains.Inequalities]
C:43 [in Waterproof.Libs.Negation]
c:45 [in Waterproof.Chains.Inequalities]
C:46 [in Waterproof.Libs.Negation]
c:46 [in Waterproof.Libs.Analysis.Sequences]
C:49 [in Waterproof.Libs.Negation]
c:49 [in Waterproof.Chains.Inequalities]
C:5 [in Waterproof.Tactics.Either]
c:5 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
C:52 [in Waterproof.Libs.Negation]
c:52 [in Waterproof.Chains.Inequalities]
c:55 [in Waterproof.Chains.Inequalities]
C:58 [in Waterproof.Chains.Inequalities]
C:7 [in Waterproof.Libs.Negation]
c:72 [in Waterproof.Chains.Inequalities]
c:75 [in Waterproof.Chains.Inequalities]
c:87 [in Waterproof.Chains.Inequalities]
c:91 [in Waterproof.Chains.Inequalities]

D

D:111 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
D:12 [in Waterproof.Libs.Negation]
d:122 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
d:127 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
d:132 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
d:136 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
d:140 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
d:142 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
d:145 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
D:28 [in Waterproof.Libs.Negation]
D:32 [in Waterproof.Libs.Negation]
D:36 [in Waterproof.Libs.Negation]
D:4 [in Waterproof.Libs.Negation]
D:40 [in Waterproof.Libs.Negation]
D:8 [in Waterproof.Libs.Negation]

E

ecn:167 [in Waterproof.Chains.Inequalities]
ecn:175 [in Waterproof.Chains.Inequalities]
ecn:191 [in Waterproof.Chains.Inequalities]
ecn:207 [in Waterproof.Chains.Inequalities]
ecn:215 [in Waterproof.Chains.Inequalities]
ecn:231 [in Waterproof.Chains.Inequalities]
ecx:169 [in Waterproof.Chains.Inequalities]
ecx:177 [in Waterproof.Chains.Inequalities]
ecx:193 [in Waterproof.Chains.Inequalities]
ecx:209 [in Waterproof.Chains.Inequalities]
ecx:217 [in Waterproof.Chains.Inequalities]
ecx:233 [in Waterproof.Chains.Inequalities]
eps:62 [in Waterproof.Libs.Analysis.Sequences]
eps:80 [in Waterproof.Libs.Analysis.Sequences]
eps:83 [in Waterproof.Libs.Analysis.Sequences]
EqualInterpretation0:71 [in Waterproof.Chains.Inequalities]
EqualInterpretation0:74 [in Waterproof.Chains.Inequalities]
EqualInterpretation0:79 [in Waterproof.Chains.Inequalities]
E:112 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
e:123 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
e:128 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
e:133 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
e:137 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
e:141 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
e:144 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
e:147 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
e:148 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
e:150 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]

F

f:100 [in Waterproof.Libs.Analysis.Subsequences]
f:108 [in Waterproof.Libs.Analysis.Subsequences]
f:115 [in Waterproof.Libs.Analysis.Subsequences]
f:119 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
f:125 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
f:13 [in Waterproof.Libs.Analysis.ContinuityDomainR]
f:130 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
f:135 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
f:139 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
f:142 [in Waterproof.Chains.Inequalities]
f:143 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
f:146 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
f:148 [in Waterproof.Chains.Inequalities]
f:154 [in Waterproof.Chains.Inequalities]
f:161 [in Waterproof.Chains.Inequalities]
f:20 [in Waterproof.Libs.Analysis.ContinuityDomainNat]
f:22 [in Waterproof.Libs.Analysis.Subsequences]
f:26 [in Waterproof.Libs.Analysis.ContinuityDomainNat]
f:6 [in Waterproof.Libs.Analysis.Subsequences]
f:62 [in Waterproof.Libs.Analysis.Subsequences]
f:7 [in Waterproof.Libs.Analysis.ContinuityDomainR]
f:96 [in Waterproof.Libs.Analysis.Subsequences]

G

gcn:195 [in Waterproof.Chains.Inequalities]
gcn:199 [in Waterproof.Chains.Inequalities]
gcn:235 [in Waterproof.Chains.Inequalities]
gcn:239 [in Waterproof.Chains.Inequalities]
gcx:197 [in Waterproof.Chains.Inequalities]
gcx:201 [in Waterproof.Chains.Inequalities]
gcx:237 [in Waterproof.Chains.Inequalities]
gcx:241 [in Waterproof.Chains.Inequalities]
g:104 [in Waterproof.Libs.Analysis.Subsequences]
g:106 [in Waterproof.Libs.Analysis.Subsequences]
g:112 [in Waterproof.Libs.Analysis.Subsequences]
g:119 [in Waterproof.Libs.Analysis.Subsequences]
G:12 [in Waterproof.Util.Goals]
g:13 [in Waterproof.Libs.Analysis.Subsequences]
G:15 [in Waterproof.Util.Goals]
G:18 [in Waterproof.Util.Goals]
g:18 [in Waterproof.Libs.Analysis.SubsequencesMetric]
G:2 [in Waterproof.Util.Goals]
g:20 [in Waterproof.Libs.Analysis.SubsequencesMetric]
G:21 [in Waterproof.Util.Goals]
G:24 [in Waterproof.Util.Goals]
g:26 [in Waterproof.Libs.Analysis.Subsequences]
G:29 [in Waterproof.Util.Goals]
g:33 [in Waterproof.Libs.Analysis.Subsequences]
G:34 [in Waterproof.Util.Goals]
G:38 [in Waterproof.Util.Goals]
G:42 [in Waterproof.Util.Goals]
G:45 [in Waterproof.Util.Goals]
G:48 [in Waterproof.Util.Goals]
g:50 [in Waterproof.Libs.Analysis.Subsequences]
G:6 [in Waterproof.Util.Goals]
g:64 [in Waterproof.Libs.Analysis.Subsequences]
G:9 [in Waterproof.Util.Goals]

H

Hstep:101 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
Hstep:160 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
Hstep:23 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
Hstep:57 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
HypP:17 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
HypP:49 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
H0:154 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
H0:19 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
H0:51 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
H0:95 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
h:18 [in Waterproof.Libs.Analysis.Subsequences]
h:18 [in Waterproof.Libs.Analysis.ContinuityDomainR]
h:28 [in Waterproof.Util.Goals]
h:28 [in Waterproof.Libs.Analysis.ContinuityDomainNat]
h:33 [in Waterproof.Util.Goals]

I

ii:10 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
ii:16 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
ii:23 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
ii:51 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
ii:92 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
i:15 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
i:22 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
i:30 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
i:50 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
i:81 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
i:9 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
i:91 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]

K

k0:20 [in Waterproof.Libs.Analysis.SequentialAccumulationPoints]
k0:74 [in Waterproof.Libs.Analysis.Subsequences]
k0:77 [in Waterproof.Libs.Analysis.Subsequences]
k1:28 [in Waterproof.Libs.Analysis.SubsequencesMetric]
k2:29 [in Waterproof.Libs.Analysis.SubsequencesMetric]
k:100 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:102 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:103 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
k:104 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:105 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
k:105 [in Waterproof.Libs.Analysis.Subsequences]
k:107 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
K:107 [in Waterproof.Libs.Analysis.SupAndInf]
k:108 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:11 [in Waterproof.Libs.Analysis.SequentialAccumulationPoints]
k:11 [in Waterproof.Libs.Analysis.Subsequences]
k:11 [in Waterproof.Libs.Analysis.SubsequencesMetric]
k:112 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:114 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:114 [in Waterproof.Libs.Analysis.Subsequences]
k:116 [in Waterproof.Libs.Analysis.Subsequences]
k:12 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
k:12 [in Waterproof.Libs.Analysis.SequentialAccumulationPoints]
k:120 [in Waterproof.Libs.Analysis.Subsequences]
k:121 [in Waterproof.Libs.Analysis.Subsequences]
k:122 [in Waterproof.Libs.Analysis.Subsequences]
k:13 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:13 [in Waterproof.Libs.Analysis.SequentialAccumulationPoints]
k:14 [in Waterproof.Libs.Analysis.SequentialAccumulationPoints]
k:14 [in Waterproof.Libs.Analysis.SequencesMetric]
k:15 [in Waterproof.Libs.Analysis.SequentialAccumulationPoints]
k:15 [in Waterproof.Libs.Analysis.Subsequences]
k:155 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
k:16 [in Waterproof.Libs.Analysis.SequentialAccumulationPoints]
k:16 [in Waterproof.Libs.Analysis.SubsequencesMetric]
k:162 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
k:166 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
k:168 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
k:170 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
k:176 [in Waterproof.Libs.Analysis.SupAndInf]
k:178 [in Waterproof.Libs.Analysis.SupAndInf]
K:18 [in Waterproof.Libs.Analysis.Sequences]
k:185 [in Waterproof.Libs.Analysis.SupAndInf]
k:19 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:19 [in Waterproof.Libs.Analysis.SequentialAccumulationPoints]
k:19 [in Waterproof.Libs.Analysis.SubsequencesMetric]
k:19 [in Waterproof.Libs.Analysis.Series]
k:190 [in Waterproof.Libs.Analysis.SupAndInf]
k:194 [in Waterproof.Libs.Analysis.SupAndInf]
k:195 [in Waterproof.Libs.Analysis.SupAndInf]
k:2 [in Waterproof.Libs.Analysis.SubsequencesMetric]
k:2 [in Waterproof.Libs.Analysis.Series]
k:20 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
k:21 [in Waterproof.Libs.Analysis.Subsequences]
k:21 [in Waterproof.Libs.Analysis.SubsequencesMetric]
k:23 [in Waterproof.Libs.Analysis.SubsequencesMetric]
k:24 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
k:24 [in Waterproof.Libs.Analysis.SubsequencesMetric]
k:25 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:25 [in Waterproof.Libs.Analysis.Sequences]
k:26 [in Waterproof.Libs.Analysis.SubsequencesMetric]
k:28 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:29 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
k:3 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
k:30 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
k:30 [in Waterproof.Libs.Analysis.SubsequencesMetric]
k:31 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
k:31 [in Waterproof.Libs.Analysis.Subsequences]
k:33 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:34 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:34 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
k:36 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:37 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:37 [in Waterproof.Libs.Analysis.Subsequences]
k:37 [in Waterproof.Libs.Analysis.SubsequencesMetric]
k:38 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:39 [in Waterproof.Libs.Analysis.SubsequencesMetric]
k:4 [in Waterproof.Libs.Analysis.SequentialAccumulationPoints]
k:4 [in Waterproof.Libs.Analysis.SubsequencesMetric]
k:40 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:41 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:43 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:44 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
k:44 [in Waterproof.Libs.Analysis.Subsequences]
k:44 [in Waterproof.Libs.Analysis.SubsequencesMetric]
k:45 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:45 [in Waterproof.Libs.Analysis.SubsequencesMetric]
k:46 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:46 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
k:46 [in Waterproof.Libs.Analysis.Subsequences]
k:46 [in Waterproof.Libs.Analysis.SubsequencesMetric]
k:47 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:48 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:49 [in Waterproof.Libs.Analysis.Subsequences]
k:49 [in Waterproof.Libs.Analysis.SubsequencesMetric]
k:5 [in Waterproof.Libs.Analysis.Subsequences]
k:5 [in Waterproof.Libs.Analysis.SubsequencesMetric]
k:5 [in Waterproof.Libs.Analysis.Sequences]
K:50 [in Waterproof.Libs.Analysis.SubsequencesMetric]
k:51 [in Waterproof.Libs.Analysis.SubsequencesMetric]
k:52 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
k:53 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:55 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:57 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:57 [in Waterproof.Libs.Analysis.Subsequences]
k:58 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:58 [in Waterproof.Libs.Analysis.Subsequences]
k:59 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:59 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
k:6 [in Waterproof.Libs.Analysis.SubsequencesMetric]
k:60 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:61 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:61 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
k:62 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:63 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:63 [in Waterproof.Libs.Analysis.Subsequences]
k:64 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:64 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
k:65 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:65 [in Waterproof.Libs.Analysis.Subsequences]
k:66 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:67 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:67 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
k:67 [in Waterproof.Libs.Analysis.Subsequences]
k:68 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:68 [in Waterproof.Libs.Analysis.Subsequences]
k:69 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:70 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:70 [in Waterproof.Libs.Analysis.Subsequences]
k:72 [in Waterproof.Libs.Analysis.Subsequences]
k:73 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
k:73 [in Waterproof.Libs.Analysis.Subsequences]
k:74 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:76 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:76 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
k:76 [in Waterproof.Libs.Analysis.Subsequences]
k:77 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:77 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
k:78 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:79 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:79 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
k:79 [in Waterproof.Libs.Analysis.Subsequences]
k:8 [in Waterproof.Libs.Analysis.Sequences]
k:81 [in Waterproof.Libs.Analysis.Subsequences]
K:81 [in Waterproof.Libs.Analysis.SupAndInf]
k:82 [in Waterproof.Libs.Analysis.Subsequences]
k:84 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
k:85 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:85 [in Waterproof.Libs.Analysis.Subsequences]
k:86 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:87 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
K:88 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
k:89 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
K:90 [in Waterproof.Libs.Analysis.SupAndInf]
k:95 [in Waterproof.Libs.Analysis.Subsequences]
k:96 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
k:98 [in Waterproof.Libs.Analysis.Subsequences]
K:99 [in Waterproof.Libs.Analysis.SupAndInf]

L

lcn:179 [in Waterproof.Chains.Inequalities]
lcn:183 [in Waterproof.Chains.Inequalities]
lcn:219 [in Waterproof.Chains.Inequalities]
lcn:223 [in Waterproof.Chains.Inequalities]
lcx:181 [in Waterproof.Chains.Inequalities]
lcx:185 [in Waterproof.Chains.Inequalities]
lcx:221 [in Waterproof.Chains.Inequalities]
lcx:225 [in Waterproof.Chains.Inequalities]
ln:166 [in Waterproof.Chains.Inequalities]
ln:170 [in Waterproof.Chains.Inequalities]
ln:174 [in Waterproof.Chains.Inequalities]
ln:178 [in Waterproof.Chains.Inequalities]
ln:182 [in Waterproof.Chains.Inequalities]
ln:186 [in Waterproof.Chains.Inequalities]
ln:190 [in Waterproof.Chains.Inequalities]
ln:194 [in Waterproof.Chains.Inequalities]
ln:198 [in Waterproof.Chains.Inequalities]
ln:202 [in Waterproof.Chains.Inequalities]
ln:206 [in Waterproof.Chains.Inequalities]
ln:210 [in Waterproof.Chains.Inequalities]
ln:214 [in Waterproof.Chains.Inequalities]
ln:218 [in Waterproof.Chains.Inequalities]
ln:222 [in Waterproof.Chains.Inequalities]
ln:226 [in Waterproof.Chains.Inequalities]
ln:230 [in Waterproof.Chains.Inequalities]
ln:234 [in Waterproof.Chains.Inequalities]
ln:238 [in Waterproof.Chains.Inequalities]
ln:242 [in Waterproof.Chains.Inequalities]
lx:164 [in Waterproof.Chains.Inequalities]
lx:168 [in Waterproof.Chains.Inequalities]
lx:172 [in Waterproof.Chains.Inequalities]
lx:176 [in Waterproof.Chains.Inequalities]
lx:184 [in Waterproof.Chains.Inequalities]
lx:188 [in Waterproof.Chains.Inequalities]
lx:192 [in Waterproof.Chains.Inequalities]
lx:200 [in Waterproof.Chains.Inequalities]
lx:204 [in Waterproof.Chains.Inequalities]
lx:208 [in Waterproof.Chains.Inequalities]
lx:212 [in Waterproof.Chains.Inequalities]
lx:216 [in Waterproof.Chains.Inequalities]
lx:224 [in Waterproof.Chains.Inequalities]
lx:228 [in Waterproof.Chains.Inequalities]
lx:232 [in Waterproof.Chains.Inequalities]
lx:240 [in Waterproof.Chains.Inequalities]
l:10 [in Waterproof.Libs.Analysis.Series]
l:101 [in Waterproof.Libs.Analysis.Subsequences]
L:106 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
l:109 [in Waterproof.Libs.Analysis.Subsequences]
l:12 [in Waterproof.Libs.Analysis.Sequences]
l:12 [in Waterproof.Libs.Analysis.Series]
l:14 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
l:147 [in Waterproof.Libs.Analysis.SupAndInf]
l:148 [in Waterproof.Libs.Analysis.SupAndInf]
l:15 [in Waterproof.Libs.Analysis.SupAndInf]
l:157 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
l:157 [in Waterproof.Libs.Analysis.SupAndInf]
l:158 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
l:158 [in Waterproof.Libs.Analysis.SupAndInf]
l:159 [in Waterproof.Libs.Analysis.SupAndInf]
l:16 [in Waterproof.Libs.Analysis.Subsequences]
l:16 [in Waterproof.Libs.Analysis.Series]
l:171 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
l:20 [in Waterproof.Libs.Analysis.Series]
L:21 [in Waterproof.Libs.Analysis.Series]
l:22 [in Waterproof.Libs.Analysis.SubsequencesMetric]
l:22 [in Waterproof.Libs.Analysis.Sequences]
L:22 [in Waterproof.Libs.Analysis.ContinuityDomainNat]
l:23 [in Waterproof.Libs.Analysis.Subsequences]
l:25 [in Waterproof.Libs.Analysis.SubsequencesMetric]
l:3 [in Waterproof.Libs.Analysis.Series]
l:36 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
l:38 [in Waterproof.Libs.Analysis.SupAndInf]
l:40 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
l:41 [in Waterproof.Libs.Analysis.SupAndInf]
l:45 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
l:47 [in Waterproof.Libs.Analysis.Sequences]
l:54 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
l:56 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
L:56 [in Waterproof.Libs.Analysis.SupAndInf]
L:58 [in Waterproof.Libs.Analysis.Sequences]
l:6 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
l:62 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
l:63 [in Waterproof.Libs.Analysis.SupAndInf]
l:65 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
l:66 [in Waterproof.Libs.Analysis.Subsequences]
L:67 [in Waterproof.Libs.Analysis.SupAndInf]
L:68 [in Waterproof.Libs.Analysis.Sequences]
l:69 [in Waterproof.Libs.Analysis.Subsequences]
l:73 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
L:73 [in Waterproof.Libs.Analysis.SupAndInf]
l:77 [in Waterproof.Libs.Analysis.Sequences]
L:79 [in Waterproof.Libs.Analysis.SupAndInf]
l:80 [in Waterproof.Libs.Analysis.Subsequences]
l:81 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
l:82 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
L:82 [in Waterproof.Libs.Analysis.SupAndInf]
l:83 [in Waterproof.Libs.Analysis.Subsequences]
l:86 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
l:88 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
L:88 [in Waterproof.Libs.Analysis.SupAndInf]
l:89 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
l:9 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
l:90 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
l:90 [in Waterproof.Libs.Analysis.Subsequences]
l:91 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
L:91 [in Waterproof.Libs.Analysis.SupAndInf]
l:92 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
l:97 [in Waterproof.Libs.Analysis.Subsequences]
l:98 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
l:99 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
l:99 [in Waterproof.Libs.Analysis.Subsequences]

M

m_seq:56 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
M0:131 [in Waterproof.Libs.Analysis.SupAndInf]
M0:132 [in Waterproof.Libs.Analysis.SupAndInf]
M0:139 [in Waterproof.Libs.Analysis.SupAndInf]
M0:140 [in Waterproof.Libs.Analysis.SupAndInf]
M0:36 [in Waterproof.Libs.Analysis.SupAndInf]
M0:37 [in Waterproof.Libs.Analysis.SupAndInf]
M0:42 [in Waterproof.Libs.Analysis.SupAndInf]
M0:53 [in Waterproof.Libs.Analysis.SupAndInf]
M0:57 [in Waterproof.Libs.Analysis.SupAndInf]
M0:60 [in Waterproof.Libs.Analysis.SupAndInf]
M0:64 [in Waterproof.Libs.Analysis.SupAndInf]
M1:101 [in Waterproof.Libs.Analysis.Sequences]
M1:108 [in Waterproof.Libs.Analysis.Sequences]
M1:99 [in Waterproof.Libs.Analysis.Sequences]
M:1 [in Waterproof.Libs.Analysis.SequencesMetric]
m:10 [in Waterproof.Libs.Analysis.SubsequencesMetric]
M:10 [in Waterproof.Libs.Analysis.SequencesMetric]
m:10 [in Waterproof.Libs.Analysis.ContinuityDomainNat]
m:104 [in Waterproof.Libs.Analysis.SupAndInf]
M:105 [in Waterproof.Libs.Analysis.Sequences]
m:109 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
m:11 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
M:112 [in Waterproof.Libs.Analysis.SupAndInf]
M:113 [in Waterproof.Libs.Analysis.Sequences]
m:115 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
m:116 [in Waterproof.Libs.Analysis.SupAndInf]
M:117 [in Waterproof.Libs.Analysis.Sequences]
m:12 [in Waterproof.Libs.Analysis.Subsequences]
m:12 [in Waterproof.Libs.Analysis.SupAndInf]
m:12 [in Waterproof.Libs.Analysis.ContinuityDomainNat]
m:120 [in Waterproof.Libs.Analysis.Sequences]
M:120 [in Waterproof.Libs.Analysis.SupAndInf]
M:123 [in Waterproof.Libs.Analysis.Sequences]
m:124 [in Waterproof.Libs.Analysis.SupAndInf]
M:127 [in Waterproof.Libs.Analysis.Sequences]
M:128 [in Waterproof.Libs.Analysis.SupAndInf]
m:14 [in Waterproof.Libs.Analysis.SubsequencesMetric]
M:14 [in Waterproof.Libs.Analysis.Sequences]
m:14 [in Waterproof.Libs.Analysis.SupAndInf]
m:144 [in Waterproof.Libs.Analysis.SupAndInf]
M:161 [in Waterproof.Libs.Analysis.SupAndInf]
M:168 [in Waterproof.Libs.Analysis.SupAndInf]
m:17 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
m:17 [in Waterproof.Libs.Analysis.Subsequences]
m:171 [in Waterproof.Libs.Analysis.SupAndInf]
m:184 [in Waterproof.Libs.Analysis.SupAndInf]
m:188 [in Waterproof.Libs.Analysis.SupAndInf]
M:19 [in Waterproof.Libs.Analysis.SupAndInf]
m:192 [in Waterproof.Libs.Analysis.SupAndInf]
m:2 [in Waterproof.Libs.Analysis.ContinuityDomainNat]
m:22 [in Waterproof.Libs.Analysis.SupAndInf]
m:25 [in Waterproof.Libs.Analysis.SupAndInf]
m:26 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
m:27 [in Waterproof.Libs.Analysis.Subsequences]
m:29 [in Waterproof.Libs.Analysis.Subsequences]
M:29 [in Waterproof.Libs.Analysis.SupAndInf]
m:3 [in Waterproof.Libs.Analysis.Subsequences]
m:3 [in Waterproof.Libs.Analysis.ContinuityDomainNat]
M:31 [in Waterproof.Libs.Analysis.Series]
M:32 [in Waterproof.Libs.Analysis.SupAndInf]
m:33 [in Waterproof.Libs.Analysis.SupAndInf]
m:35 [in Waterproof.Libs.Analysis.Subsequences]
M:35 [in Waterproof.Libs.Analysis.SupAndInf]
m:38 [in Waterproof.Libs.Analysis.Subsequences]
M:4 [in Waterproof.Libs.Analysis.Series]
m:42 [in Waterproof.Libs.Analysis.Subsequences]
m:43 [in Waterproof.Libs.Analysis.SubsequencesMetric]
M:45 [in Waterproof.Libs.Analysis.Series]
m:46 [in Waterproof.Libs.Analysis.SupAndInf]
m:47 [in Waterproof.Libs.Analysis.Subsequences]
m:48 [in Waterproof.Libs.Analysis.SupAndInf]
M:49 [in Waterproof.Libs.Analysis.SupAndInf]
M:5 [in Waterproof.Libs.Analysis.SupAndInf]
m:5 [in Waterproof.Libs.Analysis.ContinuityDomainNat]
m:51 [in Waterproof.Libs.Analysis.Subsequences]
M:51 [in Waterproof.Libs.Analysis.SupAndInf]
m:53 [in Waterproof.Libs.Analysis.Subsequences]
m:54 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
m:55 [in Waterproof.Libs.Analysis.Subsequences]
M:55 [in Waterproof.Libs.Analysis.SupAndInf]
M:56 [in Waterproof.Libs.Analysis.Subsequences]
m:59 [in Waterproof.Libs.Analysis.Subsequences]
M:59 [in Waterproof.Libs.Analysis.Sequences]
m:59 [in Waterproof.Libs.Analysis.SupAndInf]
m:6 [in Waterproof.Libs.Analysis.SequentialAccumulationPoints]
M:60 [in Waterproof.Libs.Analysis.Subsequences]
M:61 [in Waterproof.Libs.Analysis.Subsequences]
m:62 [in Waterproof.Libs.Analysis.SupAndInf]
M:66 [in Waterproof.Libs.Analysis.SupAndInf]
M:69 [in Waterproof.Libs.Analysis.Sequences]
m:7 [in Waterproof.Libs.Analysis.SequentialAccumulationPoints]
m:7 [in Waterproof.Libs.Analysis.Subsequences]
M:7 [in Waterproof.Libs.Analysis.SupAndInf]
m:72 [in Waterproof.Libs.Analysis.SupAndInf]
m:76 [in Waterproof.Libs.Analysis.Sequences]
M:78 [in Waterproof.Libs.Analysis.SupAndInf]
m:8 [in Waterproof.Libs.Analysis.ContinuityDomainNat]
m:83 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
m:87 [in Waterproof.Libs.Analysis.SupAndInf]
M:9 [in Waterproof.Libs.Analysis.SequentialAccumulationPoints]
m:9 [in Waterproof.Libs.Analysis.Subsequences]
m:9 [in Waterproof.Libs.Analysis.SupAndInf]
M:92 [in Waterproof.Libs.Analysis.Sequences]
m:95 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
M:95 [in Waterproof.Libs.Analysis.Sequences]
M:96 [in Waterproof.Libs.Analysis.SupAndInf]

N

Na:53 [in Waterproof.Libs.Analysis.Sequences]
Nc:55 [in Waterproof.Libs.Analysis.Sequences]
Nn:193 [in Waterproof.Libs.Analysis.SupAndInf]
Nn:22 [in Waterproof.Libs.Analysis.Series]
Nn:23 [in Waterproof.Libs.Analysis.Series]
Nn:24 [in Waterproof.Libs.Analysis.Series]
Nn:25 [in Waterproof.Libs.Analysis.Series]
Nn:26 [in Waterproof.Libs.Analysis.Series]
Nn:28 [in Waterproof.Libs.Analysis.Series]
Nn:29 [in Waterproof.Libs.Analysis.Series]
Nn:30 [in Waterproof.Libs.Analysis.Series]
Nn:31 [in Waterproof.Libs.Analysis.Sequences]
Nn:33 [in Waterproof.Libs.Analysis.Series]
Nn:34 [in Waterproof.Libs.Analysis.Series]
Nn:35 [in Waterproof.Libs.Analysis.Series]
Nn:36 [in Waterproof.Libs.Analysis.Series]
Nn:37 [in Waterproof.Libs.Analysis.Series]
Nn:38 [in Waterproof.Libs.Analysis.Series]
Nn:39 [in Waterproof.Libs.Analysis.Series]
Nn:40 [in Waterproof.Libs.Analysis.Series]
Nn:43 [in Waterproof.Libs.Analysis.Series]
Nn:44 [in Waterproof.Libs.Analysis.Series]
Nn:51 [in Waterproof.Libs.Analysis.Sequences]
Nn:65 [in Waterproof.Libs.Analysis.Sequences]
n_kplus1:159 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
n_0:153 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
n_kplus1:100 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
n_0:94 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
n_kplus1:87 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
n_kplus1:83 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
n_ge_k:16 [in Waterproof.Libs.Analysis.SequencesMetric]
n0:163 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
n0:164 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
N0:36 [in Waterproof.Libs.Analysis.SubsequencesMetric]
n0:75 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
N1:124 [in Waterproof.Libs.Analysis.Sequences]
N1:128 [in Waterproof.Libs.Analysis.Sequences]
N1:16 [in Waterproof.Libs.Analysis.Sequences]
N1:38 [in Waterproof.Libs.Analysis.SubsequencesMetric]
n1:38 [in Waterproof.Libs.Analysis.Sequences]
N1:5 [in Waterproof.Libs.Analysis.SequencesMetric]
N1:86 [in Waterproof.Libs.Analysis.Sequences]
N2:88 [in Waterproof.Libs.Analysis.Sequences]
N3:48 [in Waterproof.Libs.Analysis.SubsequencesMetric]
n:1 [in Waterproof.Tactics.Induction]
n:1 [in Waterproof.Libs.Analysis.SubsequencesMetric]
n:1 [in Waterproof.Libs.Analysis.Sequences]
n:1 [in Waterproof.Libs.Analysis.ContinuityDomainNat]
n:10 [in Waterproof.Libs.Analysis.SequentialAccumulationPoints]
N:10 [in Waterproof.Libs.Analysis.Subsequences]
n:100 [in Waterproof.Libs.Analysis.Sequences]
n:101 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
n:102 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
n:102 [in Waterproof.Libs.Analysis.Sequences]
n:103 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
n:103 [in Waterproof.Libs.Analysis.Sequences]
n:104 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
n:104 [in Waterproof.Libs.Analysis.Sequences]
n:106 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
n:106 [in Waterproof.Libs.Analysis.Sequences]
N:107 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
n:107 [in Waterproof.Libs.Analysis.Subsequences]
n:107 [in Waterproof.Libs.Analysis.Sequences]
n:109 [in Waterproof.Libs.Analysis.Sequences]
n:11 [in Waterproof.Libs.Analysis.SequencesMetric]
n:11 [in Waterproof.Libs.Analysis.ContinuityDomainNat]
n:110 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
n:110 [in Waterproof.Libs.Analysis.Sequences]
N:111 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
n:111 [in Waterproof.Libs.Analysis.Sequences]
N:113 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
n:113 [in Waterproof.Libs.Analysis.Subsequences]
n:114 [in Waterproof.Libs.Analysis.Sequences]
n:115 [in Waterproof.Libs.Analysis.Sequences]
n:116 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
n:118 [in Waterproof.Libs.Analysis.Sequences]
n:121 [in Waterproof.Libs.Analysis.Sequences]
n:125 [in Waterproof.Libs.Analysis.Sequences]
n:129 [in Waterproof.Libs.Analysis.Sequences]
N:14 [in Waterproof.Libs.Analysis.Subsequences]
n:14 [in Waterproof.Libs.Analysis.Series]
n:15 [in Waterproof.Libs.Analysis.SubsequencesMetric]
n:15 [in Waterproof.Libs.Analysis.Sequences]
n:15 [in Waterproof.Libs.Analysis.SequencesMetric]
n:156 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
n:16 [in Waterproof.Libs.Analysis.ContinuityDomainNat]
n:161 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
n:163 [in Waterproof.Chains.Inequalities]
n:165 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
n:167 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
n:169 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
n:17 [in Waterproof.Libs.Analysis.SubsequencesMetric]
n:17 [in Waterproof.Libs.Analysis.Sequences]
n:17 [in Waterproof.Libs.Analysis.Series]
n:171 [in Waterproof.Chains.Inequalities]
n:181 [in Waterproof.Libs.Analysis.SupAndInf]
n:187 [in Waterproof.Chains.Inequalities]
N:189 [in Waterproof.Libs.Analysis.SupAndInf]
N:19 [in Waterproof.Libs.Analysis.Subsequences]
n:19 [in Waterproof.Libs.Analysis.Sequences]
n:19 [in Waterproof.Libs.Analysis.ContinuityDomainNat]
n:2 [in Waterproof.Libs.Analysis.Sequences]
n:20 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
n:20 [in Waterproof.Libs.Analysis.Subsequences]
n:203 [in Waterproof.Chains.Inequalities]
n:211 [in Waterproof.Chains.Inequalities]
n:227 [in Waterproof.Chains.Inequalities]
n:23 [in Waterproof.Libs.Analysis.Sequences]
n:24 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
n:24 [in Waterproof.Libs.Analysis.Sequences]
n:25 [in Waterproof.Libs.Analysis.ContinuityDomainNat]
n:26 [in Waterproof.Libs.Analysis.Sequences]
n:27 [in Waterproof.Libs.Analysis.SubsequencesMetric]
N:27 [in Waterproof.Libs.Analysis.Series]
N:28 [in Waterproof.Libs.Analysis.Subsequences]
n:28 [in Waterproof.Libs.Analysis.Sequences]
n:3 [in Waterproof.Libs.Analysis.SequentialAccumulationPoints]
n:3 [in Waterproof.Libs.Analysis.SubsequencesMetric]
N:30 [in Waterproof.Libs.Analysis.Subsequences]
n:31 [in Waterproof.Libs.Analysis.SubsequencesMetric]
n:32 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
n:32 [in Waterproof.Libs.Analysis.Sequences]
n:32 [in Waterproof.Libs.Analysis.Series]
n:33 [in Waterproof.Libs.Analysis.Sequences]
n:34 [in Waterproof.Libs.Analysis.SubsequencesMetric]
n:34 [in Waterproof.Libs.Analysis.Sequences]
N:36 [in Waterproof.Libs.Analysis.Subsequences]
N:36 [in Waterproof.Libs.Analysis.Sequences]
n:37 [in Waterproof.Libs.Analysis.Sequences]
N:39 [in Waterproof.Libs.Analysis.Subsequences]
n:39 [in Waterproof.Libs.Analysis.Sequences]
N:4 [in Waterproof.Notations.Reals]
N:4 [in Waterproof.Libs.Analysis.Subsequences]
n:4 [in Waterproof.Libs.Analysis.Sequences]
n:4 [in Waterproof.Libs.Analysis.ContinuityDomainNat]
n:40 [in Waterproof.Libs.Analysis.Sequences]
n:41 [in Waterproof.Libs.Analysis.Sequences]
N:41 [in Waterproof.Libs.Analysis.Series]
n:42 [in Waterproof.Libs.Analysis.Sequences]
N:42 [in Waterproof.Libs.Analysis.Series]
n:43 [in Waterproof.Libs.Analysis.Sequences]
n:44 [in Waterproof.Libs.Analysis.ContinuityDomainNat]
n:45 [in Waterproof.Libs.Analysis.Subsequences]
n:45 [in Waterproof.Libs.Analysis.ContinuityDomainNat]
n:46 [in Waterproof.Libs.Analysis.Series]
n:47 [in Waterproof.Libs.Analysis.Series]
N:48 [in Waterproof.Libs.Analysis.Subsequences]
n:48 [in Waterproof.Libs.Analysis.Sequences]
n:48 [in Waterproof.Libs.Analysis.Series]
n:49 [in Waterproof.Libs.Analysis.Sequences]
n:49 [in Waterproof.Libs.Analysis.Series]
n:5 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
n:5 [in Waterproof.Notations.Reals]
n:50 [in Waterproof.Libs.Analysis.Series]
N:51 [in Waterproof.Libs.Analysis.Series]
n:52 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
N:52 [in Waterproof.Libs.Analysis.Subsequences]
n:52 [in Waterproof.Libs.Analysis.Sequences]
N:52 [in Waterproof.Libs.Analysis.Series]
N:54 [in Waterproof.Libs.Analysis.Subsequences]
n:54 [in Waterproof.Libs.Analysis.Sequences]
n:56 [in Waterproof.Libs.Analysis.Sequences]
n:6 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
n:6 [in Waterproof.Libs.Analysis.SequencesMetric]
n:6 [in Waterproof.Libs.Analysis.Series]
n:6 [in Waterproof.Libs.Analysis.ContinuityDomainNat]
n:60 [in Waterproof.Libs.Analysis.Sequences]
n:61 [in Waterproof.Libs.Analysis.Sequences]
N:63 [in Waterproof.Libs.Analysis.Sequences]
n:64 [in Waterproof.Libs.Analysis.Sequences]
n:66 [in Waterproof.Libs.Analysis.Sequences]
n:68 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
n:7 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
n:7 [in Waterproof.Libs.Analysis.Series]
n:7 [in Waterproof.Libs.Analysis.ContinuityDomainNat]
n:70 [in Waterproof.Libs.Analysis.Sequences]
n:71 [in Waterproof.Libs.Analysis.Subsequences]
n:71 [in Waterproof.Libs.Analysis.Sequences]
n:72 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
n:72 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
n:72 [in Waterproof.Libs.Analysis.Sequences]
n:73 [in Waterproof.Libs.Analysis.Sequences]
n:75 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
n:75 [in Waterproof.Libs.Analysis.Subsequences]
n:78 [in Waterproof.Libs.Analysis.Subsequences]
n:78 [in Waterproof.Libs.Analysis.Sequences]
n:79 [in Waterproof.Libs.Analysis.Sequences]
N:8 [in Waterproof.Libs.Analysis.Subsequences]
n:8 [in Waterproof.Libs.Analysis.Series]
n:80 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
N:81 [in Waterproof.Libs.Analysis.Sequences]
n:82 [in Waterproof.Libs.Analysis.Sequences]
n:84 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
N:84 [in Waterproof.Libs.Analysis.Sequences]
n:85 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
n:85 [in Waterproof.Libs.Analysis.Sequences]
N:86 [in Waterproof.Libs.Analysis.Subsequences]
n:87 [in Waterproof.Libs.Analysis.Sequences]
n:89 [in Waterproof.Libs.Analysis.Sequences]
n:9 [in Waterproof.Libs.Analysis.Sequences]
n:9 [in Waterproof.Libs.Analysis.ContinuityDomainNat]
N:91 [in Waterproof.Libs.Analysis.Subsequences]
n:93 [in Waterproof.Libs.Analysis.Sequences]
N:94 [in Waterproof.Libs.Analysis.Subsequences]
n:96 [in Waterproof.Libs.Analysis.Sequences]
n:97 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
n:99 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
N₀:12 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
N₀:18 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
N₀:31 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
N₀:43 [in Waterproof.Libs.Analysis.Subsequences]

O

OrderInterpretation0:102 [in Waterproof.Chains.Inequalities]
OrderInterpretation0:105 [in Waterproof.Chains.Inequalities]
OrderInterpretation0:110 [in Waterproof.Chains.Inequalities]
OrderInterpretation0:112 [in Waterproof.Chains.Inequalities]
OrderInterpretation0:115 [in Waterproof.Chains.Inequalities]
OrderInterpretation0:118 [in Waterproof.Chains.Inequalities]
OrderInterpretation0:123 [in Waterproof.Chains.Inequalities]
OrderInterpretation0:99 [in Waterproof.Chains.Inequalities]

P

prev:21 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
prev:53 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
pr1:2 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
pr2:3 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
pr:174 [in Waterproof.Libs.Analysis.SupAndInf]
pr:183 [in Waterproof.Libs.Analysis.SupAndInf]
pr:187 [in Waterproof.Libs.Analysis.SupAndInf]
pr:191 [in Waterproof.Libs.Analysis.SupAndInf]
P:1 [in Waterproof.Libs.Logic.InformativeEpsilon]
P:1 [in Waterproof.Libs.Logic.ConstructiveLogic]
p:1 [in Waterproof.Libs.Analysis.OpenAndClosed]
P:11 [in Waterproof.Libs.Logic.ConstructiveLogic]
P:113 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
p:12 [in Waterproof.Libs.Analysis.SubsequencesMetric]
P:14 [in Waterproof.Libs.Negation]
P:14 [in Waterproof.Libs.Logic.ConstructiveLogic]
P:16 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
P:17 [in Waterproof.Libs.Logic.ConstructiveLogic]
P:2 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
P:2 [in Waterproof.Libs.Analysis.Subsequences]
P:20 [in Waterproof.Libs.Negation]
P:20 [in Waterproof.Libs.Logic.ConstructiveLogic]
P:3 [in Waterproof.Libs.Logic.ConstructiveLogic]
P:33 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
p:33 [in Waterproof.Libs.Analysis.SubsequencesMetric]
P:34 [in Waterproof.Libs.Analysis.Subsequences]
P:38 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
P:41 [in Waterproof.Libs.Analysis.Subsequences]
P:42 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
p:42 [in Waterproof.Libs.Analysis.SubsequencesMetric]
P:48 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
P:5 [in Waterproof.Libs.Logic.ConstructiveLogic]
P:54 [in Waterproof.Libs.Negation]
P:60 [in Waterproof.Libs.Negation]
P:66 [in Waterproof.Libs.Negation]
P:72 [in Waterproof.Libs.Negation]
P:8 [in Waterproof.Libs.Logic.ConstructiveLogic]
P:93 [in Waterproof.Libs.Analysis.Subsequences]

Q

q:112 [in Waterproof.Libs.Analysis.Sequences]
Q:12 [in Waterproof.Libs.Logic.ConstructiveLogic]
Q:15 [in Waterproof.Libs.Negation]
Q:15 [in Waterproof.Libs.Logic.ConstructiveLogic]
Q:152 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
Q:18 [in Waterproof.Libs.Logic.ConstructiveLogic]
Q:2 [in Waterproof.Libs.Logic.InformativeEpsilon]
Q:2 [in Waterproof.Libs.Logic.ConstructiveLogic]
Q:21 [in Waterproof.Libs.Negation]
Q:21 [in Waterproof.Libs.Logic.ConstructiveLogic]
Q:4 [in Waterproof.Libs.Logic.ConstructiveLogic]
Q:55 [in Waterproof.Libs.Negation]
Q:6 [in Waterproof.Libs.Logic.ConstructiveLogic]
Q:61 [in Waterproof.Libs.Negation]
Q:66 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
Q:67 [in Waterproof.Libs.Negation]
Q:70 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
Q:71 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
Q:73 [in Waterproof.Libs.Negation]
Q:74 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
Q:78 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
Q:9 [in Waterproof.Libs.Logic.ConstructiveLogic]
q:9 [in Waterproof.Libs.Analysis.SequencesMetric]
q:9 [in Waterproof.Libs.Analysis.ContinuityDomainR]
q:91 [in Waterproof.Libs.Analysis.Sequences]
Q:93 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
q:98 [in Waterproof.Libs.Analysis.Sequences]

R

rel1:80 [in Waterproof.Chains.Inequalities]
rel1:83 [in Waterproof.Chains.Inequalities]
rel2:81 [in Waterproof.Chains.Inequalities]
rel2:84 [in Waterproof.Chains.Inequalities]
rel:124 [in Waterproof.Chains.Inequalities]
rel:128 [in Waterproof.Chains.Inequalities]
rel:132 [in Waterproof.Chains.Inequalities]
rel:136 [in Waterproof.Chains.Inequalities]
rel:67 [in Waterproof.Chains.Inequalities]
rel:84 [in Waterproof.Libs.Analysis.Subsequences]
rel:89 [in Waterproof.Libs.Analysis.Subsequences]
r1:11 [in Waterproof.Libs.Reals]
r1:14 [in Waterproof.Libs.Reals]
r1:22 [in Waterproof.Libs.Reals]
r1:24 [in Waterproof.Libs.Reals]
r1:26 [in Waterproof.Libs.Reals]
r1:28 [in Waterproof.Libs.Reals]
r1:9 [in Waterproof.Libs.Reals]
r2:10 [in Waterproof.Libs.Reals]
r2:12 [in Waterproof.Libs.Reals]
r2:15 [in Waterproof.Libs.Reals]
r2:23 [in Waterproof.Libs.Reals]
r2:25 [in Waterproof.Libs.Reals]
r2:27 [in Waterproof.Libs.Reals]
r2:29 [in Waterproof.Libs.Reals]
R:10 [in Waterproof.Libs.Logic.ConstructiveLogic]
R:13 [in Waterproof.Libs.Logic.ConstructiveLogic]
r:13 [in Waterproof.Libs.Reals]
R:16 [in Waterproof.Libs.Logic.ConstructiveLogic]
r:16 [in Waterproof.Libs.Analysis.ContinuityDomainR]
R:19 [in Waterproof.Libs.Logic.ConstructiveLogic]
r:2 [in Waterproof.Libs.Analysis.OpenAndClosed]
R:22 [in Waterproof.Libs.Logic.ConstructiveLogic]
r:6 [in Waterproof.Libs.Analysis.OpenAndClosed]
R:7 [in Waterproof.Libs.Logic.ConstructiveLogic]

S

seq:13 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
seq:25 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
seq:28 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
seq:35 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
seq:39 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
seq:43 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
seq:58 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
seq:60 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
seq:63 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]

T

T:1 [in Waterproof.Util.Assertions]
T:1 [in Waterproof.Util.Init]
T:10 [in Waterproof.Chains.Inequalities]
T:101 [in Waterproof.Chains.Inequalities]
T:104 [in Waterproof.Chains.Inequalities]
T:109 [in Waterproof.Chains.Inequalities]
T:111 [in Waterproof.Chains.Inequalities]
T:114 [in Waterproof.Chains.Inequalities]
T:117 [in Waterproof.Chains.Inequalities]
T:122 [in Waterproof.Chains.Inequalities]
T:13 [in Waterproof.Chains.Inequalities]
T:21 [in Waterproof.Chains.Inequalities]
T:22 [in Waterproof.Chains.Inequalities]
T:23 [in Waterproof.Chains.Inequalities]
T:24 [in Waterproof.Chains.Inequalities]
T:25 [in Waterproof.Chains.Inequalities]
T:26 [in Waterproof.Chains.Inequalities]
T:27 [in Waterproof.Chains.Inequalities]
T:33 [in Waterproof.Chains.Inequalities]
T:34 [in Waterproof.Chains.Inequalities]
T:35 [in Waterproof.Chains.Inequalities]
T:36 [in Waterproof.Chains.Inequalities]
T:40 [in Waterproof.Chains.Inequalities]
T:44 [in Waterproof.Chains.Inequalities]
T:48 [in Waterproof.Chains.Inequalities]
T:51 [in Waterproof.Chains.Inequalities]
T:54 [in Waterproof.Chains.Inequalities]
T:57 [in Waterproof.Chains.Inequalities]
T:63 [in Waterproof.Chains.Inequalities]
T:66 [in Waterproof.Chains.Inequalities]
T:7 [in Waterproof.Chains.Inequalities]
T:70 [in Waterproof.Chains.Inequalities]
T:73 [in Waterproof.Chains.Inequalities]
T:78 [in Waterproof.Chains.Inequalities]
T:86 [in Waterproof.Chains.Inequalities]
T:90 [in Waterproof.Chains.Inequalities]
T:94 [in Waterproof.Chains.Inequalities]
T:98 [in Waterproof.Chains.Inequalities]

U

U:4 [in Waterproof.Notations.Sets]
U:5 [in Waterproof.Notations.Sets]

V

v:1 [in Waterproof.Tactics.Help]
v:2 [in Waterproof.Tactics.Help]

X

x0:17 [in Waterproof.Libs.Analysis.SequentialAccumulationPoints]
x0:18 [in Waterproof.Libs.Analysis.SequentialAccumulationPoints]
x:1 [in Waterproof.Util.Constr]
X:1 [in Waterproof.Notations.Sets]
x:1 [in Waterproof.Libs.Reals]
x:1 [in Waterproof.Notations.Common]
X:1 [in Waterproof.Libs.Analysis.MetricSpaces]
x:11 [in Waterproof.Libs.Analysis.OpenAndClosed]
x:11 [in Waterproof.Libs.Analysis.MetricSpaces]
X:12 [in Waterproof.Libs.Analysis.SequencesMetric]
x:12 [in Waterproof.Libs.Analysis.ContinuityDomainR]
x:12 [in Waterproof.Libs.Analysis.MetricSpaces]
x:125 [in Waterproof.Chains.Inequalities]
x:129 [in Waterproof.Chains.Inequalities]
x:13 [in Waterproof.Util.Goals]
x:133 [in Waterproof.Chains.Inequalities]
x:137 [in Waterproof.Chains.Inequalities]
x:14 [in Waterproof.Libs.Analysis.OpenAndClosed]
x:14 [in Waterproof.Libs.Analysis.MetricSpaces]
x:16 [in Waterproof.Libs.Negation]
x:16 [in Waterproof.Libs.Reals]
x:16 [in Waterproof.Libs.Analysis.OpenAndClosed]
x:16 [in Waterproof.Libs.Analysis.MetricSpaces]
x:165 [in Waterproof.Chains.Inequalities]
x:17 [in Waterproof.Libs.Negation]
x:17 [in Waterproof.Libs.Reals]
x:17 [in Waterproof.Libs.Analysis.ContinuityDomainR]
x:17 [in Waterproof.Libs.Analysis.SupAndInf]
x:173 [in Waterproof.Chains.Inequalities]
x:18 [in Waterproof.Libs.Negation]
x:180 [in Waterproof.Chains.Inequalities]
x:189 [in Waterproof.Chains.Inequalities]
x:19 [in Waterproof.Util.Goals]
x:196 [in Waterproof.Chains.Inequalities]
x:2 [in Waterproof.Util.Assertions]
x:2 [in Waterproof.Libs.Analysis.SequentialAccumulationPoints]
x:2 [in Waterproof.Libs.Analysis.SupAndInf]
x:2 [in Waterproof.Util.Init]
x:2 [in Waterproof.Libs.Analysis.MetricSpaces]
x:205 [in Waterproof.Chains.Inequalities]
x:213 [in Waterproof.Chains.Inequalities]
x:22 [in Waterproof.Libs.Negation]
x:22 [in Waterproof.Libs.Analysis.ContinuityDomainR]
x:220 [in Waterproof.Chains.Inequalities]
x:229 [in Waterproof.Chains.Inequalities]
x:23 [in Waterproof.Libs.Negation]
x:236 [in Waterproof.Chains.Inequalities]
x:24 [in Waterproof.Libs.Negation]
x:25 [in Waterproof.Util.Goals]
x:25 [in Waterproof.Libs.Analysis.ContinuityDomainR]
x:27 [in Waterproof.Libs.Analysis.ContinuityDomainR]
x:28 [in Waterproof.Libs.Analysis.ContinuityDomainR]
x:3 [in Waterproof.Libs.Analysis.Sequences]
x:3 [in Waterproof.Libs.Reals]
x:3 [in Waterproof.Libs.Analysis.OpenAndClosed]
x:3 [in Waterproof.Libs.Analysis.ContinuityDomainR]
x:3 [in Waterproof.Notations.Common]
x:30 [in Waterproof.Libs.Analysis.ContinuityDomainR]
x:32 [in Waterproof.Libs.Analysis.ContinuityDomainNat]
x:33 [in Waterproof.Libs.Analysis.ContinuityDomainR]
x:35 [in Waterproof.Util.Goals]
x:35 [in Waterproof.Libs.Analysis.ContinuityDomainNat]
x:36 [in Waterproof.Libs.Analysis.ContinuityDomainR]
x:36 [in Waterproof.Libs.Analysis.ContinuityDomainNat]
x:39 [in Waterproof.Libs.Analysis.ContinuityDomainNat]
x:4 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
x:4 [in Waterproof.Libs.Analysis.MetricSpaces]
x:40 [in Waterproof.Libs.Analysis.SubsequencesMetric]
x:40 [in Waterproof.Libs.Analysis.SupAndInf]
x:42 [in Waterproof.Libs.Analysis.ContinuityDomainNat]
x:43 [in Waterproof.Util.Goals]
x:44 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
x:45 [in Waterproof.Libs.Analysis.SupAndInf]
x:49 [in Waterproof.Util.Goals]
x:5 [in Waterproof.Libs.Reals]
x:5 [in Waterproof.Notations.Common]
x:56 [in Waterproof.Libs.Negation]
x:57 [in Waterproof.Libs.Negation]
x:58 [in Waterproof.Libs.Negation]
x:6 [in Waterproof.Notations.Reals]
x:6 [in Waterproof.Notations.Sets]
x:6 [in Waterproof.Libs.Analysis.ContinuityDomainR]
x:6 [in Waterproof.Libs.Analysis.SupAndInf]
x:6 [in Waterproof.Libs.Analysis.MetricSpaces]
x:62 [in Waterproof.Libs.Negation]
x:63 [in Waterproof.Libs.Negation]
x:64 [in Waterproof.Libs.Negation]
x:68 [in Waterproof.Libs.Negation]
x:68 [in Waterproof.Chains.Inequalities]
x:69 [in Waterproof.Libs.Negation]
x:7 [in Waterproof.Util.Goals]
x:7 [in Waterproof.Notations.Reals]
X:7 [in Waterproof.Libs.Analysis.SequencesMetric]
x:7 [in Waterproof.Libs.Reals]
x:7 [in Waterproof.Libs.Analysis.OpenAndClosed]
x:7 [in Waterproof.Notations.Common]
x:70 [in Waterproof.Libs.Negation]
x:70 [in Waterproof.Libs.Analysis.SupAndInf]
x:74 [in Waterproof.Libs.Negation]
x:75 [in Waterproof.Libs.Negation]
x:76 [in Waterproof.Libs.Negation]
x:76 [in Waterproof.Libs.Analysis.SupAndInf]
x:8 [in Waterproof.Notations.Reals]
x:8 [in Waterproof.Libs.Analysis.SequentialAccumulationPoints]
x:8 [in Waterproof.Libs.Analysis.MetricSpaces]
x:81 [in Waterproof.Libs.Negation]
x:82 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
x:82 [in Waterproof.Libs.Negation]
x:83 [in Waterproof.Libs.Negation]
x:84 [in Waterproof.Libs.Negation]
x:85 [in Waterproof.Libs.Negation]
x:86 [in Waterproof.Libs.Negation]
x:87 [in Waterproof.Libs.Negation]
x:88 [in Waterproof.Libs.Negation]
x:89 [in Waterproof.Libs.Negation]
x:9 [in Waterproof.Notations.Reals]
x:9 [in Waterproof.Notations.Common]
x:90 [in Waterproof.Libs.Negation]
x:91 [in Waterproof.Libs.Negation]
x:92 [in Waterproof.Libs.Negation]
x:94 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
x:97 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
x:98 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]

Y

y:10 [in Waterproof.Notations.Common]
y:126 [in Waterproof.Chains.Inequalities]
y:13 [in Waterproof.Libs.Analysis.MetricSpaces]
y:130 [in Waterproof.Chains.Inequalities]
y:134 [in Waterproof.Chains.Inequalities]
y:138 [in Waterproof.Chains.Inequalities]
y:15 [in Waterproof.Libs.Analysis.MetricSpaces]
y:17 [in Waterproof.Libs.Analysis.MetricSpaces]
y:180 [in Waterproof.Libs.Analysis.SupAndInf]
y:2 [in Waterproof.Libs.Reals]
y:2 [in Waterproof.Notations.Common]
y:27 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
y:3 [in Waterproof.Libs.Analysis.MetricSpaces]
y:4 [in Waterproof.Libs.Reals]
y:4 [in Waterproof.Notations.Common]
y:41 [in Waterproof.Libs.Analysis.SubsequencesMetric]
y:5 [in Waterproof.Libs.Analysis.MetricSpaces]
y:6 [in Waterproof.Libs.Reals]
y:6 [in Waterproof.Notations.Common]
y:69 [in Waterproof.Chains.Inequalities]
y:7 [in Waterproof.Libs.Analysis.MetricSpaces]
y:8 [in Waterproof.Libs.Reals]
y:8 [in Waterproof.Notations.Common]
y:9 [in Waterproof.Libs.Analysis.MetricSpaces]

Z

z:10 [in Waterproof.Libs.Analysis.MetricSpaces]
z:162 [in Waterproof.Chains.Inequalities]
z:47 [in Waterproof.Libs.Analysis.SupAndInf]

other

δ1:26 [in Waterproof.Libs.Analysis.ContinuityDomainR]
δ:11 [in Waterproof.Libs.Analysis.ContinuityDomainR]
δ:21 [in Waterproof.Libs.Analysis.ContinuityDomainR]
δ:24 [in Waterproof.Libs.Analysis.ContinuityDomainR]
δ:24 [in Waterproof.Libs.Analysis.ContinuityDomainNat]
δ:31 [in Waterproof.Libs.Analysis.ContinuityDomainNat]
δ:32 [in Waterproof.Libs.Analysis.ContinuityDomainR]
δ:34 [in Waterproof.Libs.Analysis.ContinuityDomainNat]
δ:35 [in Waterproof.Libs.Analysis.ContinuityDomainR]
δ:38 [in Waterproof.Libs.Analysis.ContinuityDomainNat]
δ:41 [in Waterproof.Libs.Analysis.ContinuityDomainNat]
ε:10 [in Waterproof.Libs.Analysis.ContinuityDomainR]
ε:100 [in Waterproof.Libs.Analysis.SupAndInf]
ε:105 [in Waterproof.Libs.Analysis.SupAndInf]
ε:108 [in Waterproof.Libs.Analysis.SupAndInf]
ε:113 [in Waterproof.Libs.Analysis.SupAndInf]
ε:117 [in Waterproof.Libs.Analysis.SupAndInf]
ε:121 [in Waterproof.Libs.Analysis.SupAndInf]
ε:125 [in Waterproof.Libs.Analysis.SupAndInf]
ε:129 [in Waterproof.Libs.Analysis.SupAndInf]
ε:13 [in Waterproof.Libs.Analysis.Sequences]
ε:133 [in Waterproof.Libs.Analysis.SupAndInf]
ε:135 [in Waterproof.Libs.Analysis.SupAndInf]
ε:137 [in Waterproof.Libs.Analysis.SupAndInf]
ε:141 [in Waterproof.Libs.Analysis.SupAndInf]
ε:145 [in Waterproof.Libs.Analysis.SupAndInf]
ε:149 [in Waterproof.Libs.Analysis.SupAndInf]
ε:15 [in Waterproof.Libs.Analysis.ContinuityDomainNat]
ε:151 [in Waterproof.Libs.Analysis.SupAndInf]
ε:153 [in Waterproof.Libs.Analysis.SupAndInf]
ε:155 [in Waterproof.Libs.Analysis.SupAndInf]
ε:175 [in Waterproof.Libs.Analysis.SupAndInf]
ε:177 [in Waterproof.Libs.Analysis.SupAndInf]
ε:18 [in Waterproof.Libs.Analysis.ContinuityDomainNat]
ε:2 [in Waterproof.Libs.Analysis.ContinuityDomainR]
ε:20 [in Waterproof.Libs.Analysis.ContinuityDomainR]
ε:23 [in Waterproof.Libs.Analysis.ContinuityDomainR]
ε:23 [in Waterproof.Libs.Analysis.ContinuityDomainNat]
ε:29 [in Waterproof.Libs.Analysis.ContinuityDomainR]
ε:3 [in Waterproof.Notations.Reals]
ε:30 [in Waterproof.Libs.Analysis.Sequences]
ε:30 [in Waterproof.Libs.Analysis.ContinuityDomainNat]
ε:31 [in Waterproof.Libs.Analysis.ContinuityDomainR]
ε:33 [in Waterproof.Libs.Analysis.ContinuityDomainNat]
ε:34 [in Waterproof.Libs.Analysis.ContinuityDomainR]
ε:35 [in Waterproof.Libs.Analysis.SubsequencesMetric]
ε:35 [in Waterproof.Libs.Analysis.Sequences]
ε:37 [in Waterproof.Libs.Analysis.ContinuityDomainNat]
ε:4 [in Waterproof.Libs.Analysis.SequencesMetric]
ε:40 [in Waterproof.Libs.Analysis.ContinuityDomainNat]
ε:43 [in Waterproof.Libs.Analysis.ContinuityDomainNat]
ε:47 [in Waterproof.Libs.Analysis.SubsequencesMetric]
ε:5 [in Waterproof.Libs.Analysis.ContinuityDomainR]
ε:50 [in Waterproof.Libs.Analysis.Sequences]
ε:97 [in Waterproof.Libs.Analysis.SupAndInf]

Module Index

B

ByContradiction [in Waterproof.Util.Goals]

C

Case [in Waterproof.Util.Goals]

H

HelpNewHyp [in Waterproof.Tactics.Help]

N

NaturalInduction [in Waterproof.Util.Goals]
NaturalInduction.Base [in Waterproof.Util.Goals]
NaturalInduction.Step [in Waterproof.Util.Goals]

S

StateGoal [in Waterproof.Util.Goals]
StateHyp [in Waterproof.Util.Goals]
StrongIndIndxSeq [in Waterproof.Util.Goals]

Variable Index

M

metricspace.X [in Waterproof.Libs.Analysis.ContinuityDomainNat]
my_section.X [in Waterproof.Libs.Analysis.SubsequencesMetric]

Library Index

A

Analysis
Assertions
Assume
Automation

B

Because
Binders
BothDirections
BothStatements

C

Chains
Choose
Claims
Common
Conclusion
Constr
ConstructiveLogic
ContinuityDomainNat
ContinuityDomainR
Contradiction

D

Define

E

G

Goals

H

Help
Hints
Hypothesis

I

Induction
Inequalities
InformativeEpsilon
Init
ItHolds
ItSuffices

L

LimsupLiminfBolzano

M

Manipulation
MessagesToUser
MetricSpaces

N

Negation
Notations

O

Obtain
OpenAndClosed

R

S

Sequences
SequencesMetric
SequentialAccumulationPoints
Series
Sets
Since
Specialize
StrongInductionIndexSequence
Subsequences
SubsequencesMetric
SupAndInf

T

Tactics
Take
ToShow
TypeCorrector

U

Unfold

V

W

Waterproof
Waterprove

Lemma Index

A

acc_pt_bds_seq_ub [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
all_not_ex_func [in Waterproof.Libs.Negation]
all_func [in Waterproof.Libs.Negation]
alt_char_continuity [in Waterproof.Libs.Analysis.ContinuityDomainR]
alt_char_inf [in Waterproof.Libs.Analysis.SupAndInf]
alt_char_sup [in Waterproof.Libs.Analysis.SupAndInf]
alt_char_continuity [in Waterproof.Libs.Analysis.ContinuityDomainNat]
and_not_impl_func [in Waterproof.Libs.Negation]
and_not_or_func [in Waterproof.Libs.Negation]
and_func [in Waterproof.Libs.Negation]
any_low_bd_le_inf [in Waterproof.Libs.Analysis.SupAndInf]
any_upp_bd_ge_sup [in Waterproof.Libs.Analysis.SupAndInf]
archimed_mod [in Waterproof.Libs.Analysis.Sequences]
aux1 [in Waterproof.Libs.Analysis.ContinuityDomainNat]

B

bdd_below_to_bdd_above_set_opp [in Waterproof.Libs.Analysis.SupAndInf]
Bolzano_Weierstrass [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
Bolzano_Weierstrass_gen [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
bounded_by_lower_bound_propform [in Waterproof.Libs.Analysis.SupAndInf]
bounded_by_upper_bound_propform [in Waterproof.Libs.Analysis.SupAndInf]
built_seq_is_index_seq [in Waterproof.Libs.Analysis.Subsequences]

C

classic_strong_ind_index_seq_with_prop [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
convergence_equivalence [in Waterproof.Libs.Analysis.Sequences]
conv_evt_eq_seq [in Waterproof.Libs.Analysis.Sequences]
created_seq_is_index_seq [in Waterproof.Libs.Analysis.Subsequences]

D

dep_only_on_start_index_seq_prop_family [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
div_pos [in Waterproof.Libs.Reals]
div_sign_flip [in Waterproof.Libs.Reals]
double_sumbool_sumtriad_cba [in Waterproof.Tactics.Either]
double_sumbool_sumtriad_cab [in Waterproof.Tactics.Either]
double_sumbool_sumtriad_bca [in Waterproof.Tactics.Either]
double_sumbool_sumtriad_bac [in Waterproof.Tactics.Either]
double_sumbool_sumtriad_acb [in Waterproof.Tactics.Either]
double_sumbool_sumtriad_abc [in Waterproof.Tactics.Either]
double_is_even [in Waterproof.Libs.Analysis.SubsequencesMetric]
d'_eq_3 [in Waterproof.Libs.Analysis.MetricSpaces]
d'_eq_0 [in Waterproof.Libs.Analysis.MetricSpaces]

E

elements_le_seq_of_max [in Waterproof.Libs.Analysis.Subsequences]
elements_le_seq_of_max_pre [in Waterproof.Libs.Analysis.Subsequences]
equivalent_subsequence_convergence [in Waterproof.Libs.Analysis.SubsequencesMetric]
eq_seq_conv_to_same_lim [in Waterproof.Libs.Analysis.Sequences]
every_point_in_R_acc_point_R [in Waterproof.Libs.Analysis.ContinuityDomainR]
existence_next_el_to_fun [in Waterproof.Libs.Analysis.Subsequences]
exists_subseq_to_limsup_bdd [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
exists_almost_lim_sup [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
exists_good_subseq [in Waterproof.Libs.Analysis.Subsequences]
exists_almost_lim_sup_aux [in Waterproof.Libs.Analysis.SupAndInf]
exists_almost_minimizer_ε [in Waterproof.Libs.Analysis.SupAndInf]
exists_almost_maximizer_ε [in Waterproof.Libs.Analysis.SupAndInf]
exists_almost_minimizer [in Waterproof.Libs.Analysis.SupAndInf]
exists_almost_maximizer [in Waterproof.Libs.Analysis.SupAndInf]
exists_inf [in Waterproof.Libs.Analysis.SupAndInf]
ex_not_all_func [in Waterproof.Libs.Negation]
ex_func [in Waterproof.Libs.Negation]

F

false_Req [in Waterproof.Libs.Reals]
finite_or_find_one [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]

H

help_with_choice [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]

I

if_almost_minimizer_ε_then_every_low_bd_smaller [in Waterproof.Libs.Analysis.SupAndInf]
if_almost_maximizer_ε_then_every_upp_bd_larger [in Waterproof.Libs.Analysis.SupAndInf]
if_almost_minimizer_then_every_low_bd_smaller [in Waterproof.Libs.Analysis.SupAndInf]
if_almost_maximizer_then_every_upp_bd_larger [in Waterproof.Libs.Analysis.SupAndInf]
impl_not_and_func [in Waterproof.Libs.Negation]
impl_func [in Waterproof.Libs.Negation]
incr_loc_to_glob [in Waterproof.Libs.Analysis.Subsequences]
incr_loc_to_glob [in Waterproof.Libs.Analysis.SubsequencesMetric]
index_seq_grows [in Waterproof.Libs.Analysis.Subsequences]
index_seq_grows_0 [in Waterproof.Libs.Analysis.Subsequences]
index_seq_strictly_incr [in Waterproof.Libs.Analysis.Subsequences]
index_sequence_property2 [in Waterproof.Libs.Analysis.SubsequencesMetric]
index_seq_equiv [in Waterproof.Libs.Analysis.SubsequencesMetric]
index_sequence_property [in Waterproof.Libs.Analysis.SubsequencesMetric]
informative_or_lift [in Waterproof.Libs.Logic.InformativeEpsilon]
inf_el_to_fun [in Waterproof.Libs.Analysis.Subsequences]
inf_is_low_bd [in Waterproof.Libs.Analysis.SupAndInf]
inv_remove [in Waterproof.Libs.Reals]
in_implies_not_in_compl [in Waterproof.Libs.Analysis.OpenAndClosed]
is_bounded_equivalence [in Waterproof.Libs.Analysis.Sequences]

L

left_in_closed_open [in Waterproof.Libs.Reals]
lim_sup_bdd_is_lub_seq_acc_pts [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
lim_const_min_1_over_n_plus_1 [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
lim_d_0 [in Waterproof.Libs.Analysis.Sequences]
lim_const_seq [in Waterproof.Libs.Analysis.Sequences]
low_bd_seq_is_low_bd_lim [in Waterproof.Libs.Analysis.Sequences]
low_bd_set_opp_to_upp_bd_set [in Waterproof.Libs.Analysis.SupAndInf]
low_bd_set_to_upp_bd_set_opp [in Waterproof.Libs.Analysis.SupAndInf]

M

make_sumtriad_uninformative_6 [in Waterproof.Libs.Logic.ConstructiveLogic]
make_sumtriad_uninformative_5 [in Waterproof.Libs.Logic.ConstructiveLogic]
make_sumtriad_uninformative_4 [in Waterproof.Libs.Logic.ConstructiveLogic]
make_sumtriad_uninformative_3 [in Waterproof.Libs.Logic.ConstructiveLogic]
make_sumtriad_uninformative_2 [in Waterproof.Libs.Logic.ConstructiveLogic]
make_sumtriad_uninformative_1 [in Waterproof.Libs.Logic.ConstructiveLogic]
make_sumbool_uninformative_2 [in Waterproof.Libs.Logic.ConstructiveLogic]
make_sumbool_uninformative_1 [in Waterproof.Libs.Logic.ConstructiveLogic]
max_or_strict [in Waterproof.Libs.Analysis.SupAndInf]
min_1_over_n_plus_1_to_0 [in Waterproof.Libs.Analysis.Sequences]
mouse_tail [in Waterproof.Libs.Analysis.Series]

N

nat_dist_less_than_one_iff_equal [in Waterproof.Libs.Analysis.ContinuityDomainNat]
nat_dist_larger_zero_not_equal [in Waterproof.Libs.Analysis.ContinuityDomainNat]
nat_not_equal_dist_larger_one [in Waterproof.Libs.Analysis.ContinuityDomainNat]
not_neg_pos_func [in Waterproof.Libs.Negation]
not_ex_all_func [in Waterproof.Libs.Negation]
not_all_ex_func [in Waterproof.Libs.Negation]
not_impl_and_func [in Waterproof.Libs.Negation]
not_and_impl_func [in Waterproof.Libs.Negation]
not_and_or_func [in Waterproof.Libs.Negation]
not_or_and_func [in Waterproof.Libs.Negation]
not_in_compl_implies_in [in Waterproof.Libs.Analysis.OpenAndClosed]

O

one_in_complement_interval_closed_zero_open_one [in Waterproof.Libs.Analysis.OpenAndClosed]
or_not_and_func [in Waterproof.Libs.Negation]
or_func [in Waterproof.Libs.Negation]

P

partial_sums_pos_incr [in Waterproof.Libs.Analysis.Series]
pos_not_neg_func [in Waterproof.Libs.Negation]

Q

quant_over_start_dep_only_on_start [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]

R

Rabs_left1_with_minus [in Waterproof.Libs.Reals]
Rabs_zero [in Waterproof.Libs.Reals]
Rabs_m_lt_n [in Waterproof.Libs.Analysis.ContinuityDomainNat]
Rabs_n_min_m [in Waterproof.Libs.Analysis.ContinuityDomainNat]
reformulate_step_prop_index [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
reformulate_final_prop_index [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
reformulate_base_prop_index [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
reformulate_final_prop_strong [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
reformulate_base_prop_strong [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
relation_shift [in Waterproof.Libs.Analysis.SequencesMetric]
Req_false [in Waterproof.Libs.Reals]
Req_true [in Waterproof.Libs.Reals]
Rge_lt_or_eq_dec [in Waterproof.Libs.Reals]
Rge_le_dec [in Waterproof.Libs.Reals]
Rge_min_abs [in Waterproof.Libs.Reals]
right_in_open_closed [in Waterproof.Libs.Reals]
Rle_ge_dec [in Waterproof.Libs.Reals]
Rle_abs_min [in Waterproof.Libs.Reals]
Rlt_ge_dec [in Waterproof.Libs.Reals]
Rmax_abs [in Waterproof.Libs.Reals]
R_complete [in Waterproof.Libs.Analysis.SupAndInf]

S

sequence_ub_bds [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
seq_bdd_seq_acc_pts_bdd [in Waterproof.Libs.Analysis.SequentialAccumulationPoints]
seq_of_max_is_increasing [in Waterproof.Libs.Analysis.Subsequences]
seq_ordered_lim_ordered [in Waterproof.Libs.Analysis.Sequences]
seq_ex_almost_maximizer_m [in Waterproof.Libs.Analysis.SupAndInf]
seq_ex_almost_maximizer_ε [in Waterproof.Libs.Analysis.SupAndInf]
sigma_split_v2 [in Waterproof.Libs.Analysis.Series]
Sn_eq_nplus1 [in Waterproof.Tactics.Induction]
squeeze_theorem [in Waterproof.Libs.Analysis.Sequences]
strong_ind_index_seq_with_prop [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
strong_ind_seq_with_prop [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
subsequence_of_convergent_sequence [in Waterproof.Libs.Analysis.SubsequencesMetric]
subseq_sat_rel [in Waterproof.Libs.Analysis.Subsequences]
sumbool_comm [in Waterproof.Tactics.Either]
sup_is_upp_bd [in Waterproof.Libs.Analysis.SupAndInf]
sup_set_opp_is_inf_set [in Waterproof.Libs.Analysis.SupAndInf]

T

true_Req [in Waterproof.Libs.Reals]

U

upp_bd_seq_is_upp_bd_lim [in Waterproof.Libs.Analysis.Sequences]
upp_bd_set_opp_to_low_bd_set [in Waterproof.Libs.Analysis.SupAndInf]
upp_bd_set_to_low_bd_set_opp [in Waterproof.Libs.Analysis.SupAndInf]

Z

zero_in_interval_closed_zero_open_one [in Waterproof.Libs.Analysis.OpenAndClosed]

_

_and_assoc1 [in Waterproof.Waterprove]

Constructor Index

B

base_gc [in Waterproof.Chains.Inequalities]
base_lc [in Waterproof.Chains.Inequalities]
base_ec [in Waterproof.Chains.Inequalities]
ByContradiction.wrap [in Waterproof.Util.Goals]

C

Case.wrap [in Waterproof.Util.Goals]
chain_base [in Waterproof.Chains.Inequalities]
chain_link [in Waterproof.Chains.Inequalities]
chain_ge [in Waterproof.Chains.Inequalities]
chain_gt [in Waterproof.Chains.Inequalities]
chain_le [in Waterproof.Chains.Inequalities]
chain_lt [in Waterproof.Chains.Inequalities]
chain_eq [in Waterproof.Chains.Inequalities]

L

left [in Waterproof.Tactics.Either]
link_gc_grtr [in Waterproof.Chains.Inequalities]
link_gc_eq [in Waterproof.Chains.Inequalities]
link_ec_grtr [in Waterproof.Chains.Inequalities]
link_lc_less [in Waterproof.Chains.Inequalities]
link_lc_eq [in Waterproof.Chains.Inequalities]
link_ec_less [in Waterproof.Chains.Inequalities]
link_ec_eq [in Waterproof.Chains.Inequalities]

M

middle [in Waterproof.Tactics.Either]

N

NaturalInduction.Base.wrap [in Waterproof.Util.Goals]
NaturalInduction.Step.wrap [in Waterproof.Util.Goals]

R

right [in Waterproof.Tactics.Either]

S

StateGoal.wrap [in Waterproof.Util.Goals]
StateHyp.wrap [in Waterproof.Util.Goals]
StrongIndIndxSeq.wrap [in Waterproof.Util.Goals]

Inductive Index

B

ByContradiction.Wrapper [in Waterproof.Util.Goals]

C

Case.Wrapper [in Waterproof.Util.Goals]
ChainBase [in Waterproof.Chains.Inequalities]
ChainLink [in Waterproof.Chains.Inequalities]

E

EqualChain [in Waterproof.Chains.Inequalities]
EqualRel [in Waterproof.Chains.Inequalities]

G

GreaterChain [in Waterproof.Chains.Inequalities]
GreaterRel [in Waterproof.Chains.Inequalities]

L

LessChain [in Waterproof.Chains.Inequalities]
LessRel [in Waterproof.Chains.Inequalities]

N

NaturalInduction.Base.Wrapper [in Waterproof.Util.Goals]
NaturalInduction.Step.Wrapper [in Waterproof.Util.Goals]

S

StateGoal.Wrapper [in Waterproof.Util.Goals]
StateHyp.Wrapper [in Waterproof.Util.Goals]
StrongIndIndxSeq.Wrapper [in Waterproof.Util.Goals]
sumtriad [in Waterproof.Tactics.Either]

Projection Index

C

chain_base [in Waterproof.Chains.Inequalities]
chain_link [in Waterproof.Chains.Inequalities]

E

eq_rel_to_pred [in Waterproof.Chains.Inequalities]

G

global_statement [in Waterproof.Chains.Inequalities]
grtr_rel_to_pred [in Waterproof.Chains.Inequalities]

L

less_rel_to_pred [in Waterproof.Chains.Inequalities]

P

pred [in Waterproof.Notations.Sets]

T

total_statement [in Waterproof.Chains.Inequalities]

W

weak_global_statement [in Waterproof.Chains.Inequalities]

Section Index

C

Construction [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]

D

Definitions [in Waterproof.Libs.Analysis.MetricSpaces]

M

metricspace [in Waterproof.Libs.Analysis.ContinuityDomainNat]
my_section [in Waterproof.Libs.Analysis.SubsequencesMetric]

S

StrongInduction [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
StrongInductionIndexSequence [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]

Instance Index

B

base_gc_R_Z [in Waterproof.Chains.Inequalities]
base_gc_Z_R [in Waterproof.Chains.Inequalities]
base_lc_R_Z [in Waterproof.Chains.Inequalities]
base_lc_Z_R [in Waterproof.Chains.Inequalities]
base_ec_R_Z [in Waterproof.Chains.Inequalities]
base_ec_Z_R [in Waterproof.Chains.Inequalities]
base_gc_R_nat [in Waterproof.Chains.Inequalities]
base_gc_nat_R [in Waterproof.Chains.Inequalities]
base_lc_R_nat [in Waterproof.Chains.Inequalities]
base_lc_nat_R [in Waterproof.Chains.Inequalities]
base_ec_R_nat [in Waterproof.Chains.Inequalities]
base_ec_nat_R [in Waterproof.Chains.Inequalities]
base_gc_inst [in Waterproof.Chains.Inequalities]
base_lc_inst [in Waterproof.Chains.Inequalities]
base_ec_inst [in Waterproof.Chains.Inequalities]

E

ec_interpretable [in Waterproof.Chains.Inequalities]
equal_interpretation [in Waterproof.Chains.Inequalities]

G

gc_interpretable [in Waterproof.Chains.Inequalities]

L

lc_interpretable [in Waterproof.Chains.Inequalities]
link_gc_grtr_R_Z [in Waterproof.Chains.Inequalities]
link_gc_grtr_Z_R [in Waterproof.Chains.Inequalities]
link_gc_eq_R_Z [in Waterproof.Chains.Inequalities]
link_gc_eq_Z_R [in Waterproof.Chains.Inequalities]
link_ec_grtr_R_Z [in Waterproof.Chains.Inequalities]
link_ec_grtr_Z_R [in Waterproof.Chains.Inequalities]
link_lc_less_R_Z [in Waterproof.Chains.Inequalities]
link_lc_less_Z_R [in Waterproof.Chains.Inequalities]
link_lc_eq_R_Z [in Waterproof.Chains.Inequalities]
link_lc_eq_Z_R [in Waterproof.Chains.Inequalities]
link_ec_less_R_Z [in Waterproof.Chains.Inequalities]
link_ec_less_Z_R [in Waterproof.Chains.Inequalities]
link_ec_eq_R_Z [in Waterproof.Chains.Inequalities]
link_ec_eq_Z_R [in Waterproof.Chains.Inequalities]
link_gc_grtr_R_nat [in Waterproof.Chains.Inequalities]
link_gc_grtr_nat_R [in Waterproof.Chains.Inequalities]
link_gc_eq_R_nat [in Waterproof.Chains.Inequalities]
link_gc_eq_nat_R [in Waterproof.Chains.Inequalities]
link_ec_grtr_R_nat [in Waterproof.Chains.Inequalities]
link_ec_grtr_nat_R [in Waterproof.Chains.Inequalities]
link_lc_less_R_nat [in Waterproof.Chains.Inequalities]
link_lc_less_nat_R [in Waterproof.Chains.Inequalities]
link_lc_eq_R_nat [in Waterproof.Chains.Inequalities]
link_lc_eq_nat_R [in Waterproof.Chains.Inequalities]
link_ec_less_R_nat [in Waterproof.Chains.Inequalities]
link_ec_less_nat_R [in Waterproof.Chains.Inequalities]
link_ec_eq_R_nat [in Waterproof.Chains.Inequalities]
link_ec_eq_nat_R [in Waterproof.Chains.Inequalities]
link_gc_grtr_inst [in Waterproof.Chains.Inequalities]
link_gc_eq_inst [in Waterproof.Chains.Inequalities]
link_ec_grtr_inst [in Waterproof.Chains.Inequalities]
link_lc_less_inst [in Waterproof.Chains.Inequalities]
link_lc_eq_inst [in Waterproof.Chains.Inequalities]
link_ec_less_inst [in Waterproof.Chains.Inequalities]
link_ec_eq_inst [in Waterproof.Chains.Inequalities]

O

order_interpretation_R [in Waterproof.Chains.Inequalities]
order_interpretation_nat [in Waterproof.Chains.Inequalities]

Abbreviation Index

I

is_sup [in Waterproof.Libs.Analysis.SupAndInf]
is_bounded_above [in Waterproof.Libs.Analysis.SupAndInf]

P

partial_sums [in Waterproof.Libs.Analysis.Series]

Definition Index

A

a_seq [in Waterproof.Libs.Analysis.Sequences]

B

bounded [in Waterproof.Libs.Analysis.SequencesMetric]
build_seq [in Waterproof.Libs.Analysis.Subsequences]
ByContradiction.unwrap [in Waterproof.Util.Goals]

C

Case.unwrap [in Waterproof.Util.Goals]
complement [in Waterproof.Libs.Analysis.OpenAndClosed]
constant_sequence [in Waterproof.Libs.Analysis.Sequences]
const_seq_from [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
const_seq [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
convergence [in Waterproof.Libs.Analysis.SequencesMetric]
converges_to [in Waterproof.Notations.Reals]
create_seq [in Waterproof.Libs.Analysis.Subsequences]
cv_implies_cv_abs_to_l_abs [in Waterproof.Notations.Reals]

D

d [in Waterproof.Libs.Analysis.Sequences]
dep_choice [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
dep_only_on_start [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
dist_reflexive [in Waterproof.Libs.Analysis.MetricSpaces]
dist_triangle_inequality [in Waterproof.Libs.Analysis.MetricSpaces]
dist_symmetric [in Waterproof.Libs.Analysis.MetricSpaces]
dist_non_degenerate [in Waterproof.Libs.Analysis.MetricSpaces]
dist_positive [in Waterproof.Libs.Analysis.MetricSpaces]
diverges_to_minus_infinity [in Waterproof.Libs.Analysis.Sequences]
diverges_to_plus_infinity [in Waterproof.Libs.Analysis.Sequences]
d_discrete_R [in Waterproof.Libs.Analysis.MetricSpaces]

E

ec_map [in Waterproof.Chains.Inequalities]
ec_total_statement [in Waterproof.Chains.Inequalities]
ec_global_statement [in Waterproof.Chains.Inequalities]
ec_tail [in Waterproof.Chains.Inequalities]
ec_head [in Waterproof.Chains.Inequalities]
empty [in Waterproof.Notations.Sets]
evt_eq_sequences [in Waterproof.Libs.Analysis.Sequences]

F

finite_triangle_inequalty [in Waterproof.Notations.Reals]
first_satisfying_element [in Waterproof.Libs.Analysis.Subsequences]
first_satisfying_element_helper [in Waterproof.Libs.Analysis.Subsequences]
full [in Waterproof.Notations.Sets]

G

gc_map [in Waterproof.Chains.Inequalities]
gc_total_statement [in Waterproof.Chains.Inequalities]
gc_weak_global_statement [in Waterproof.Chains.Inequalities]
gc_global_statement [in Waterproof.Chains.Inequalities]
gc_tail [in Waterproof.Chains.Inequalities]
gc_head [in Waterproof.Chains.Inequalities]
global_grtr_rel [in Waterproof.Chains.Inequalities]
global_less_rel [in Waterproof.Chains.Inequalities]
grtr_relation_flow [in Waterproof.Chains.Inequalities]

I

index_seq_prop_family [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
ind_seq_with_prop [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
ind_seq_of_seq_and_prop [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
is_seq_acc_pt [in Waterproof.Libs.Analysis.SequentialAccumulationPoints]
is_increasing [in Waterproof.Libs.Analysis.Subsequences]
is_index_seq [in Waterproof.Libs.Analysis.Subsequences]
is_increasing [in Waterproof.Libs.Analysis.SubsequencesMetric]
is_accumulation_point [in Waterproof.Libs.Analysis.SubsequencesMetric]
is_subsequence [in Waterproof.Libs.Analysis.SubsequencesMetric]
is_index_seq [in Waterproof.Libs.Analysis.SubsequencesMetric]
is_index_sequence [in Waterproof.Libs.Analysis.SubsequencesMetric]
is_bounded_below [in Waterproof.Libs.Analysis.Sequences]
is_bounded_above [in Waterproof.Libs.Analysis.Sequences]
is_bounded_equivalent [in Waterproof.Libs.Analysis.Sequences]
is_bounded [in Waterproof.Libs.Analysis.Sequences]
is_closed [in Waterproof.Libs.Analysis.OpenAndClosed]
is_open [in Waterproof.Libs.Analysis.OpenAndClosed]
is_interior_point [in Waterproof.Libs.Analysis.OpenAndClosed]
is_continuous_in [in Waterproof.Libs.Analysis.ContinuityDomainR]
is_isolated_point [in Waterproof.Libs.Analysis.ContinuityDomainR]
is_accumulation_point [in Waterproof.Libs.Analysis.ContinuityDomainR]
is_inf_alt_char [in Waterproof.Libs.Analysis.SupAndInf]
is_sup_alt_char [in Waterproof.Libs.Analysis.SupAndInf]
is_inf [in Waterproof.Libs.Analysis.SupAndInf]
is_bounded_below [in Waterproof.Libs.Analysis.SupAndInf]
is_lower_bound [in Waterproof.Libs.Analysis.SupAndInf]
is_max [in Waterproof.Libs.Analysis.SupAndInf]
is_continuous_in [in Waterproof.Libs.Analysis.ContinuityDomainNat]
is_isolated_point [in Waterproof.Libs.Analysis.ContinuityDomainNat]
is_accumulation_point [in Waterproof.Libs.Analysis.ContinuityDomainNat]

L

lc_map [in Waterproof.Chains.Inequalities]
lc_total_statement [in Waterproof.Chains.Inequalities]
lc_weak_global_statement [in Waterproof.Chains.Inequalities]
lc_global_statement [in Waterproof.Chains.Inequalities]
lc_tail [in Waterproof.Chains.Inequalities]
lc_head [in Waterproof.Chains.Inequalities]
less_relation_flow [in Waterproof.Chains.Inequalities]
limit_in_point [in Waterproof.Libs.Analysis.ContinuityDomainR]
limit_in_point [in Waterproof.Libs.Analysis.ContinuityDomainNat]
lim_sup_bdd [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]

N

NaturalInduction.Base.unwrap [in Waterproof.Util.Goals]
NaturalInduction.Step.unwrap [in Waterproof.Util.Goals]

O

open_ball [in Waterproof.Libs.Analysis.OpenAndClosed]

S

seq_of_max [in Waterproof.Libs.Analysis.Subsequences]
series_cv_abs_to [in Waterproof.Libs.Analysis.Series]
series_cv_abs [in Waterproof.Libs.Analysis.Series]
series_cv [in Waterproof.Libs.Analysis.Series]
series_cv_to [in Waterproof.Libs.Analysis.Series]
set_opp [in Waterproof.Libs.Analysis.SupAndInf]
snd_map [in Waterproof.Chains.Inequalities]
StateGoal.unwrap [in Waterproof.Util.Goals]
StateHyp.unwrap [in Waterproof.Util.Goals]
StrongIndIndxSeq.unwrap [in Waterproof.Util.Goals]

T

type_of_test_aux [in Waterproof.Util.Assertions]
type_of [in Waterproof.Util.Init]

Y

y_seq [in Waterproof.Libs.Analysis.Sequences]

Record Index

C

ChainBase [in Waterproof.Chains.Inequalities]
ChainLink [in Waterproof.Chains.Inequalities]

E

EqualInterpretation [in Waterproof.Chains.Inequalities]

I

InterpretableChain [in Waterproof.Chains.Inequalities]

O

OrderInterpretation [in Waterproof.Chains.Inequalities]

S

subset [in Waterproof.Notations.Sets]

Global Index

J

(1962 entries)

Notation Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

(121 entries)

Binder Index

J

W

_

(1392 entries)

Module Index

A

D

E

F

G

I

J

K

L

M

O

P

Q

R

T

U

V

W

X

Y

Z

_

other

(9 entries)

Variable Index

A

B

C

D

E

F

G

H

I

J

K

L

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(2 entries)

Library Index

F

J

K

P

Q

X

Y

Z

_

other

(60 entries)

Lemma Index

G

J

K

V

W

X

Y

other

(155 entries)

Constructor Index

A

D

E

F

G

H

I

J

K

O

P

Q

T

U

V

W

X

Y

Z

_

other

(27 entries)

Inductive Index

A

D

F

H

I

J

K

M

O

P

Q

R

T

U

V

W

X

Y

Z

_

other

(16 entries)

Projection Index

A

B

D

F

H

I

J

K

M

N

O

Q

R

S

U

V

X

Y

Z

_

other

(9 entries)

Section Index

A

B

E

F

G

H

I

J

K

L

N

O

P

Q

R

T

U

V

W

X

Y

Z

_

other

(6 entries)

Instance Index

A

C

D

F

H

I

J

K

M

N

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(56 entries)

Abbreviation Index

A

B

C

D

E

F

G

H

J

K

L

M

N

O

Q

R

S

T

U

V

W

X

Y

Z

_

other

(3 entries)

Definition Index

H

J

K

M

P

Q

R

U

V

W

X

Z

_

other

(100 entries)

Record Index

A

B

D

F

G

H

J

K

L

M

N

P

Q

R

T

U

V

W

X

Y

Z

_

other

(6 entries)

This page has been generated by coqdoc