Global Index

J

K

X

(852 entries)

Notation Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

R

S

T

U

V

W

X

Y

Z

_

(188 entries)

Module Index

A

D

E

F

G

I

J

K

L

M

O

P

R

T

U

W

X

Y

Z

_

other

(13 entries)

Variable Index

A

B

E

F

G

H

I

J

K

L

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(9 entries)

Library Index

J

K

P

X

Y

Z

_

other

(79 entries)

Lemma Index

J

K

V

W

X

Y

other

(241 entries)

Constructor Index

A

D

E

F

G

H

J

K

P

Q

T

U

W

X

Y

Z

_

other

(35 entries)

Inductive Index

A

D

H

J

K

M

O

P

Q

R

T

U

W

X

Y

Z

_

other

(22 entries)

Projection Index

A

B

D

F

H

I

J

K

M

O

P

Q

R

S

U

V

X

Y

Z

_

other

(13 entries)

Instance Index

A

C

D

F

H

I

J

K

M

P

Q

S

T

U

V

W

X

Y

Z

_

other

(66 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)

Abbreviation Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

Q

R

S

T

U

V

W

X

Y

Z

_

other

(1 entry)

Definition Index

J

K

M

W

X

_

other

(169 entries)

Record Index

A

B

D

F

H

J

K

M

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(10 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]
alternative_char_unique_exists [lemma, in Waterproof.Libs.Logic.Quantification]
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]
archimedN [lemma, in Waterproof.Libs.Reals.ArchimedN]
ArchimedN [library]
archimedN_exists [lemma, in Waterproof.Libs.Reals.ArchimedN]
Assertions [library]
Assume [library]
as_subset [definition, in Waterproof.Notations.Sets]
Automation [library]
aux1 [lemma, in Waterproof.Libs.Analysis.ContinuityDomainNat]
a_seq [definition, in Waterproof.Libs.Analysis.Sequences]

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]
bdd_above_bound_iff [lemma, in Waterproof.Libs.Analysis.SupAndInf]
Because [library]
bijective [definition, in Waterproof.Libs.Functions]
bijective_iff [lemma, in Waterproof.Libs.Functions]
bijective_is_surjective [lemma, in Waterproof.Libs.Functions]
bijective_is_injective [lemma, in Waterproof.Libs.Functions]
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]
BySince [library]

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_with_element_notation [lemma, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
classic_strong_ind_index_seq_with_prop [lemma, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
Closed [constructor, in Waterproof.Libs.Reals.Intervals]
Closed_Open [constructor, in Waterproof.Libs.Reals.Intervals]
Common [library]
complement [definition, in Waterproof.Libs.Analysis.OpenAndClosed]
composition [definition, in Waterproof.Libs.Functions]
Conclusion [library]
constant_sequence [definition, in Waterproof.Libs.Analysis.Sequences]
Constr [library]
Construction [section, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
Construction.A [variable, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
Construction.a0 [variable, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
Construction.Hstep [variable, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
Construction.HypP [variable, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
Construction.H0 [variable, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
Construction.P [variable, 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]
conv [definition, in Waterproof.Notations.Sets]
convergence [definition, in Waterproof.Libs.Analysis.SequencesMetric]
convergence_opp [lemma, in Waterproof.Libs.Analysis.Sequences]
convergence_minus [lemma, in Waterproof.Libs.Analysis.Sequences]
convergence_plus [lemma, in Waterproof.Libs.Analysis.Sequences]
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]

D

d [definition, in Waterproof.Libs.Analysis.Sequences]
Define [library]
Definitions [section, in Waterproof.Libs.Analysis.MetricSpaces]
Definitions.X [variable, 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]
diff_is_rational [lemma, in Waterproof.Libs.Reals.Rational]
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]
divide_char_inv [lemma, in Waterproof.Libs.Integers.Divisibility]
divide_char [lemma, in Waterproof.Libs.Integers.Divisibility]
Divisibility [library]
div_is_rational [lemma, in Waterproof.Libs.Reals.Rational]
div_one_neq_zero [lemma, in Waterproof.Libs.Reals]
div_non_zero [lemma, in Waterproof.Libs.Reals]
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]

E

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]
empty_set_characterization [lemma, in Waterproof.Libs.Sets]
EqualChain [inductive, in Waterproof.Chains.Inequalities]
EqualChain_sind [definition, in Waterproof.Chains.Inequalities]
EqualChain_rec [definition, in Waterproof.Chains.Inequalities]
EqualChain_ind [definition, in Waterproof.Chains.Inequalities]
EqualChain_rect [definition, in Waterproof.Chains.Inequalities]
EqualInterpretation [record, in Waterproof.Chains.Inequalities]
EqualRel [inductive, in Waterproof.Chains.Inequalities]
EqualRel_sind [definition, in Waterproof.Chains.Inequalities]
EqualRel_rec [definition, in Waterproof.Chains.Inequalities]
EqualRel_ind [definition, in Waterproof.Chains.Inequalities]
EqualRel_rect [definition, 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]
Even [library]
even_or_odd [lemma, in Waterproof.Libs.Integers.Even]
even_of [lemma, in Waterproof.Libs.Integers.Even]
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]
exists_exists_in_iff [lemma, in Waterproof.Notations.Sets]
ex_not_all_func [lemma, in Waterproof.Libs.Negation]
ex_func [lemma, in Waterproof.Libs.Negation]

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]
fix_earlier_warning_sind [definition, in Waterproof.Util.Goals]
fix_earlier_warning_rec [definition, in Waterproof.Util.Goals]
fix_earlier_warning_ind [definition, in Waterproof.Util.Goals]
fix_earlier_warning_rect [definition, in Waterproof.Util.Goals]
fix_earlier_warning [inductive, in Waterproof.Util.Goals]
forall_forall_in_iff [lemma, in Waterproof.Notations.Sets]
full [definition, in Waterproof.Notations.Sets]
Functions [library]
Functions [library]

G

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]
ge_zero_gt_one [lemma, in Waterproof.Libs.Reals.Integer]
ge_op [projection, in Waterproof.Notations.Sets]
ge_type [record, in Waterproof.Notations.Sets]
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]
GreaterChain_sind [definition, in Waterproof.Chains.Inequalities]
GreaterChain_rec [definition, in Waterproof.Chains.Inequalities]
GreaterChain_ind [definition, in Waterproof.Chains.Inequalities]
GreaterChain_rect [definition, in Waterproof.Chains.Inequalities]
GreaterRel [inductive, in Waterproof.Chains.Inequalities]
GreaterRel_sind [definition, in Waterproof.Chains.Inequalities]
GreaterRel_rec [definition, in Waterproof.Chains.Inequalities]
GreaterRel_ind [definition, in Waterproof.Chains.Inequalities]
GreaterRel_rect [definition, in Waterproof.Chains.Inequalities]
grtr_rel_to_pred [projection, in Waterproof.Chains.Inequalities]
grtr_relation_flow [definition, in Waterproof.Chains.Inequalities]
gt_op [projection, in Waterproof.Notations.Sets]
gt_type [record, in Waterproof.Notations.Sets]

H

has_inverse [definition, in Waterproof.Libs.Functions]
has_right_inverse [definition, in Waterproof.Libs.Functions]
has_left_inverse [definition, in Waterproof.Libs.Functions]
Help [library]
HelpNewHyp [module, in Waterproof.Tactics.Help]
help_with_choice [lemma, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
Hints [library]
Hypothesis [library]

I

id [definition, in Waterproof.Tactics.Specialize]
identity_seal [definition, in Waterproof.Notations.Common]
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]
image [definition, in Waterproof.Libs.Functions]
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]
IndexedOperations [library]
IndexedSets [library]
indexed_union_sind [definition, in Waterproof.Libs.Sets.IndexedOperations]
indexed_union_ind [definition, in Waterproof.Libs.Sets.IndexedOperations]
indexed_union [inductive, in Waterproof.Libs.Sets.IndexedOperations]
indexed_intersection_sind [definition, in Waterproof.Libs.Sets.IndexedOperations]
indexed_intersection_ind [definition, in Waterproof.Libs.Sets.IndexedOperations]
indexed_intersection [inductive, in Waterproof.Libs.Sets.IndexedOperations]
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_union_elim_left [lemma, in Waterproof.Libs.Sets.IndexedOperations]
index_union_elim [lemma, in Waterproof.Libs.Sets.IndexedOperations]
index_union_intro [constructor, in Waterproof.Libs.Sets.IndexedOperations]
index_intersection_elim_left [lemma, in Waterproof.Libs.Sets.IndexedOperations]
index_intersection_elim [lemma, in Waterproof.Libs.Sets.IndexedOperations]
index_intersection_intro [constructor, in Waterproof.Libs.Sets.IndexedOperations]
index_seq_prop_family [definition, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
index_sequence_property2_automation [lemma, in Waterproof.Libs.Analysis.SubsequencesMetric]
index_sequence_property2 [lemma, in Waterproof.Libs.Analysis.SubsequencesMetric]
index_seq_equiv [lemma, in Waterproof.Libs.Analysis.SubsequencesMetric]
index_sequence_property_automation [lemma, in Waterproof.Libs.Analysis.SubsequencesMetric]
index_sequence_property [lemma, in Waterproof.Libs.Analysis.SubsequencesMetric]
Induction [library]
induction_principle_elements [lemma, in Waterproof.Tactics.Induction]
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]
injective [definition, in Waterproof.Libs.Functions]
injective_elim [lemma, in Waterproof.Libs.Functions]
INR_0 [lemma, in Waterproof.Libs.Reals.Integer]
INR_1 [lemma, in Waterproof.Libs.Reals.Integer]
Integer [library]
Integers [library]
Integers [library]
InterpretableChain [record, in Waterproof.Chains.Inequalities]
intersection_characterization_left [lemma, in Waterproof.Libs.Sets.Operations]
intersection_characterization [lemma, in Waterproof.Libs.Sets.Operations]
Intervals [library]
int_is_rational [lemma, in Waterproof.Libs.Reals.Rational]
inverse [definition, in Waterproof.Libs.Functions]
inverse_intro [lemma, in Waterproof.Libs.Functions]
inverse_elim_right [lemma, in Waterproof.Libs.Functions]
inverse_elim_left [lemma, in Waterproof.Libs.Functions]
inverse_is_right_inverse [lemma, in Waterproof.Libs.Functions]
inverse_is_left_inverse [lemma, in Waterproof.Libs.Functions]
inv_remove [lemma, in Waterproof.Libs.Reals]
in_preimage_iff [lemma, in Waterproof.Libs.Functions]
in_preimage_elim [lemma, in Waterproof.Libs.Functions]
in_preimage_intro [lemma, in Waterproof.Libs.Functions]
in_image_iff [lemma, in Waterproof.Libs.Functions]
in_image_elim [lemma, in Waterproof.Libs.Functions]
in_image_intro [lemma, in Waterproof.Libs.Functions]
in_implies_not_in_compl [lemma, in Waterproof.Libs.Analysis.OpenAndClosed]
is_square [definition, in Waterproof.Libs.Integers.Square]
is_increasing [definition, in Waterproof.Libs.Analysis.Subsequences]
is_index_seq [definition, in Waterproof.Libs.Analysis.Subsequences]
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_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_is_lub_iff [lemma, in Waterproof.Libs.Analysis.SupAndInf]
is_upper_bound_Raxioms_is_upper_bound_iff [lemma, in Waterproof.Libs.Analysis.SupAndInf]
is_sup [definition, in Waterproof.Libs.Analysis.SupAndInf]
is_bounded_above [definition, in Waterproof.Libs.Analysis.SupAndInf]
is_upper_bound [definition, in Waterproof.Libs.Analysis.SupAndInf]
is_rational [definition, in Waterproof.Libs.Reals.Rational]
is_seq_acc_pt [definition, in Waterproof.Libs.Analysis.SequentialAccumulationPoints]
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_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_interval_sind [definition, in Waterproof.Libs.Reals.Intervals]
is_interval_ind [definition, in Waterproof.Libs.Reals.Intervals]
is_interval [inductive, in Waterproof.Libs.Reals.Intervals]
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]

L

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_inverse_intro [lemma, in Waterproof.Libs.Functions]
left_inverse_elim [lemma, in Waterproof.Libs.Functions]
left_inverse [definition, in Waterproof.Libs.Functions]
left_in_closed_open [lemma, in Waterproof.Libs.Reals]
LessChain [inductive, in Waterproof.Chains.Inequalities]
LessChain_sind [definition, in Waterproof.Chains.Inequalities]
LessChain_rec [definition, in Waterproof.Chains.Inequalities]
LessChain_ind [definition, in Waterproof.Chains.Inequalities]
LessChain_rect [definition, in Waterproof.Chains.Inequalities]
LessRel [inductive, in Waterproof.Chains.Inequalities]
LessRel_sind [definition, in Waterproof.Chains.Inequalities]
LessRel_rec [definition, in Waterproof.Chains.Inequalities]
LessRel_ind [definition, in Waterproof.Chains.Inequalities]
LessRel_rect [definition, in Waterproof.Chains.Inequalities]
less_rel_to_pred [projection, in Waterproof.Chains.Inequalities]
less_relation_flow [definition, in Waterproof.Chains.Inequalities]
le_op [projection, in Waterproof.Notations.Sets]
le_type [record, in Waterproof.Notations.Sets]
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]
Logic [library]
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]
lt_op [projection, in Waterproof.Notations.Sets]
lt_type [record, in Waterproof.Notations.Sets]

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]
mem_of_preimage [lemma, in Waterproof.Libs.Functions]
mem_subset_full_set [lemma, in Waterproof.Notations.Sets]
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]
minus_Z_in_R [lemma, in Waterproof.Libs.Reals.Integer]
min_1_over_n_plus_1_to_0 [lemma, in Waterproof.Libs.Analysis.Sequences]
min_frac [lemma, in Waterproof.Libs.Reals.Rational]
mouse_tail [lemma, in Waterproof.Libs.Analysis.Series]
mult_Z_in_R [lemma, in Waterproof.Libs.Reals.Integer]
mult_neq_zero [lemma, in Waterproof.Libs.Reals.RealInequalities]
mult_is_rational [lemma, in Waterproof.Libs.Reals.Rational]
my_section.X [variable, in Waterproof.Libs.Analysis.SubsequencesMetric]
my_section [section, in Waterproof.Libs.Analysis.SubsequencesMetric]

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_ne_type [instance, in Waterproof.Notations.Sets]
nat_lt_type [instance, in Waterproof.Notations.Sets]
nat_le_type [instance, in Waterproof.Notations.Sets]
nat_gt_type [instance, in Waterproof.Notations.Sets]
nat_ge_type [instance, in Waterproof.Notations.Sets]
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]
Negation [library]
neg_Z_in_R [lemma, in Waterproof.Libs.Reals.Integer]
neg_is_rational [lemma, in Waterproof.Libs.Reals.Rational]
ne_op [projection, in Waterproof.Notations.Sets]
ne_type [record, in Waterproof.Notations.Sets]
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_even_and_odd [lemma, in Waterproof.Libs.Integers.Even]
not_in_empty [lemma, in Waterproof.Libs.Sets]
not_in_compl_implies_in [lemma, in Waterproof.Libs.Analysis.OpenAndClosed]

O

Obtain [library]
odd_of [lemma, in Waterproof.Libs.Integers.Even]
one_Z_in_R [lemma, in Waterproof.Libs.Reals.Integer]
one_in_complement_interval_closed_zero_open_one [lemma, in Waterproof.Libs.Analysis.OpenAndClosed]
Open [constructor, in Waterproof.Libs.Reals.Intervals]
OpenAndClosed [library]
open_ball [definition, in Waterproof.Libs.Analysis.OpenAndClosed]
Open_Closed [constructor, in Waterproof.Libs.Reals.Intervals]
Operations [library]
OrderInterpretation [record, 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]
perfect_square_of [lemma, in Waterproof.Libs.Integers.Square]
plus_Z_in_R [lemma, in Waterproof.Libs.Reals.Integer]
plus_frac [lemma, in Waterproof.Libs.Reals.Rational]
pos_not_neg_func [lemma, in Waterproof.Libs.Negation]
power_set_characterization_alt [lemma, in Waterproof.Libs.Sets]
power_set_characterization [lemma, in Waterproof.Libs.Sets]
preimage [definition, in Waterproof.Libs.Functions]
preimage_of_mem [lemma, in Waterproof.Libs.Functions]

Q

Quantification [library]
Quantifiers [module, 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]
quant_over_start_dep_only_on_start [lemma, in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
Q_in_R [definition, in Waterproof.Libs.Reals.Rational]

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]
Rational [library]
rational_of [lemma, in Waterproof.Libs.Reals.Rational]
Rdivid_ineq_interchange [lemma, in Waterproof.Libs.Reals.RealInequalities]
RealInequalities [library]
Reals [library]
Reals [library]
RealsWithSubsets [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]
remainder [definition, in Waterproof.Libs.Integers.Divisibility]
remainder_of [lemma, in Waterproof.Libs.Integers.Divisibility]
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_inverse_intro [lemma, in Waterproof.Libs.Functions]
right_inverse_elim [lemma, in Waterproof.Libs.Functions]
right_inverse [definition, in Waterproof.Libs.Functions]
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_unsealed [lemma, in Waterproof.Libs.Analysis.SupAndInf]
R_complete [lemma, in Waterproof.Libs.Analysis.SupAndInf]
R_ne_type [instance, in Waterproof.Notations.Sets]
R_lt_type [instance, in Waterproof.Notations.Sets]
R_le_type [instance, in Waterproof.Notations.Sets]
R_gt_type [instance, in Waterproof.Notations.Sets]
R_ge_type [instance, in Waterproof.Notations.Sets]

S

seal [definition, in Waterproof.Notations.Sets]
Sequences [library]
SequencesMetric [library]
sequence_ub_bds [lemma, in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
SequentialAccumulationPoints [library]
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_bdd_seq_acc_pts_bdd [lemma, in Waterproof.Libs.Analysis.SequentialAccumulationPoints]
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]
Sets [library]
set_opp [definition, in Waterproof.Libs.Analysis.SupAndInf]
set_difference_elim [lemma, in Waterproof.Libs.Sets]
sigma_split_v2 [lemma, in Waterproof.Libs.Analysis.Series]
snd_map [definition, in Waterproof.Chains.Inequalities]
Sn_eq_nplus1 [lemma, in Waterproof.Tactics.Induction]
Specialize [library]
square [definition, in Waterproof.Libs.Integers.Square]
Square [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.Base [module, in Waterproof.Util.Goals]
StrongIndIndxSeq.Base.unwrap [definition, in Waterproof.Util.Goals]
StrongIndIndxSeq.Base.wrap [constructor, in Waterproof.Util.Goals]
StrongIndIndxSeq.Base.Wrapper [inductive, in Waterproof.Util.Goals]
StrongIndIndxSeq.Step [module, in Waterproof.Util.Goals]
StrongIndIndxSeq.Step.unwrap [definition, in Waterproof.Util.Goals]
StrongIndIndxSeq.Step.wrap [constructor, in Waterproof.Util.Goals]
StrongIndIndxSeq.Step.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_in [definition, in Waterproof.Notations.Sets]
subset_type [definition, in Waterproof.Notations.Sets]
sumbool_comm [lemma, in Waterproof.Tactics.Either]
sumtriad [inductive, in Waterproof.Tactics.Either]
sumtriad_sind [definition, in Waterproof.Tactics.Either]
sumtriad_rec [definition, in Waterproof.Tactics.Either]
sumtriad_ind [definition, in Waterproof.Tactics.Either]
sumtriad_rect [definition, in Waterproof.Tactics.Either]
sum_is_rational [lemma, in Waterproof.Libs.Reals.Rational]
SupAndInf [library]
sup_is_upp_bd [lemma, in Waterproof.Libs.Analysis.SupAndInf]
sup_set_opp_is_inf_set [lemma, in Waterproof.Libs.Analysis.SupAndInf]
surjective [definition, in Waterproof.Libs.Functions]
surjective_elim [lemma, in Waterproof.Libs.Functions]

T

Tactics [library]
Take [library]
ToShow [library]
total_statement [projection, in Waterproof.Chains.Inequalities]
true_Req [lemma, in Waterproof.Libs.Reals]
two_Z_in_R [lemma, in Waterproof.Libs.Reals.Integer]
TypeCorrector [library]
type_of_test_aux [definition, in Waterproof.Util.Assertions]
type_of [definition, in Waterproof.Util.Init]

U

Unfold [library]
union_characterization_left [lemma, in Waterproof.Libs.Sets.Operations]
union_characterization [lemma, in Waterproof.Libs.Sets.Operations]
unique_exists [definition, in Waterproof.Notations.Sets]
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]

V

VerifyGoal [module, in Waterproof.Util.Goals]
VerifyGoal.unwrap [definition, in Waterproof.Util.Goals]
VerifyGoal.wrap [constructor, in Waterproof.Util.Goals]
VerifyGoal.Wrapper [inductive, in Waterproof.Util.Goals]
Version [library]

W

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

Y

y_seq [definition, in Waterproof.Libs.Analysis.Sequences]

Z

zero_Z_in_R [lemma, in Waterproof.Libs.Reals.Integer]
zero_in_interval_closed_zero_open_one [lemma, in Waterproof.Libs.Analysis.OpenAndClosed]
Zeven_char_inv [lemma, in Waterproof.Libs.Integers.Even]
Zeven_char [lemma, in Waterproof.Libs.Integers.Even]
Zodd_char_inv [lemma, in Waterproof.Libs.Integers.Even]
Zodd_char [lemma, in Waterproof.Libs.Integers.Even]
Z_in_R [definition, in Waterproof.Libs.Reals.Integer]

_

_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]
< _ (chain_scope) [notation, in Waterproof.Chains.Inequalities]
_ is an inverse of _ (function_scope) [notation, in Waterproof.Notations.Functions]
_ has an inverse (function_scope) [notation, in Waterproof.Notations.Functions]
_ is a right inverse of _ (function_scope) [notation, in Waterproof.Notations.Functions]
_ has a right inverse (function_scope) [notation, in Waterproof.Notations.Functions]
_ is a left inverse of _ (function_scope) [notation, in Waterproof.Notations.Functions]
_ has a left inverse (function_scope) [notation, in Waterproof.Notations.Functions]
_ is bijective (function_scope) [notation, in Waterproof.Notations.Functions]
_ is surjective (function_scope) [notation, in Waterproof.Notations.Functions]
_ is injective (function_scope) [notation, in Waterproof.Notations.Functions]
_ ∘ _ (function_scope) [notation, in Waterproof.Notations.Functions]
_ ⁻¹ [ _ ] (function_scope) [notation, in Waterproof.Notations.Functions]
_ [ _ ] (function_scope) [notation, in Waterproof.Notations.Functions]
_ 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]
index sequence (metric_scope) [notation, in Waterproof.Libs.Analysis.SubsequencesMetric]
_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]
≠ _ (pred_for_subset_scope) [notation, in Waterproof.Notations.Sets]
≥ _ (pred_for_subset_scope) [notation, in Waterproof.Notations.Sets]
> _ (pred_for_subset_scope) [notation, in Waterproof.Notations.Sets]
≤ _ (pred_for_subset_scope) [notation, in Waterproof.Notations.Sets]
< _ (pred_for_subset_scope) [notation, in Waterproof.Notations.Sets]
∈ _ (pred_for_subset_scope) [notation, in Waterproof.Notations.Sets]
index sequence (pred_for_subset_scope) [notation, in Waterproof.Libs.Analysis.SubsequencesMetric]
_index sequence_ (pred_for_subset_scope) [notation, in Waterproof.Libs.Analysis.SubsequencesMetric]
_ is a single interval (R_scope) [notation, in Waterproof.Notations.RealsWithSubsets]
[ _ , ∞ ) (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]
｜ _ - _ ｜ (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]
_ is irrational (R2_scope) [notation, in Waterproof.Notations.RealsWithSubsets]
_ is rational (R2_scope) [notation, in Waterproof.Notations.RealsWithSubsets]
ℚ (R2_scope) [notation, in Waterproof.Notations.RealsWithSubsets]
ℤ (R2_scope) [notation, in Waterproof.Notations.RealsWithSubsets]
∃! _ _ , _ (subset_scope) [notation, in Waterproof.Notations.Sets]
{ _ , _ } (subset_scope) [notation, in Waterproof.Notations.Sets]
{ _ ∈ _ | _ } (subset_scope) [notation, in Waterproof.Notations.Sets]
for all _ _ , _ (subset_scope) [notation, in Waterproof.Notations.Sets]
∀ _ _ , _ (subset_scope) [notation, in Waterproof.Notations.Sets]
there exists _ _ , _ (subset_scope) [notation, in Waterproof.Notations.Sets]
∃ _ _ , _ (subset_scope) [notation, in Waterproof.Notations.Sets]
_ < _ (subset_scope) [notation, in Waterproof.Notations.Sets]
_ ≤ _ (subset_scope) [notation, in Waterproof.Notations.Sets]
_ > _ (subset_scope) [notation, in Waterproof.Notations.Sets]
_ ≥ _ (subset_scope) [notation, in Waterproof.Notations.Sets]
𝒫( _ ) (subset_scope) [notation, in Waterproof.Notations.Sets]
[ _ ] (subset_scope) [notation, in Waterproof.Notations.Sets]
｛ _ : _ | _ ｝ (subset_scope) [notation, in Waterproof.Notations.Sets]
_ is inhabited (subset_scope) [notation, in Waterproof.Notations.Sets]
_ is empty (subset_scope) [notation, in Waterproof.Notations.Sets]
_ is disjoint from _ (subset_scope) [notation, in Waterproof.Notations.Sets]
_ ⊂ _ (subset_scope) [notation, in Waterproof.Notations.Sets]
_ ∉ _ (subset_scope) [notation, in Waterproof.Notations.Sets]
_ \ _ (subset_scope) [notation, in Waterproof.Notations.Sets]
_ ∪ _ (subset_scope) [notation, in Waterproof.Notations.Sets]
_ ∩ _ (subset_scope) [notation, in Waterproof.Notations.Sets]
Ω (subset_scope) [notation, in Waterproof.Notations.Sets]
∅ (subset_scope) [notation, in Waterproof.Notations.Sets]
⋂_{ _ _ } _ (subset_scope) [notation, in Waterproof.Notations.IndexedSets]
_ ≠ _ (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]
_ ∨ _ (type_scope) [notation, in Waterproof.Notations.Common]
fun _ .. _ ↦ _ (type_scope) [notation, in Waterproof.Notations.Common]
_ ( _ , .. , _ ) (type_scope) [notation, in Waterproof.Notations.Common]
for all _ , _ (type_scope) [notation, in Waterproof.Notations.Sets]
∀ _ , _ (type_scope) [notation, in Waterproof.Notations.Sets]
there exists _ , _ (type_scope) [notation, in Waterproof.Notations.Sets]
∃ _ , _ (type_scope) [notation, in Waterproof.Notations.Sets]
_ ∈ _ (type_scope) [notation, in Waterproof.Notations.Sets]
_ ³ (Z_scope) [notation, in Waterproof.Notations.Integers]
_ leaves a remainder of _ when divided by _ (Z_scope) [notation, in Waterproof.Notations.Integers]
_ is a perfect square (Z_scope) [notation, in Waterproof.Notations.Integers]
_ ² (Z_scope) [notation, in Waterproof.Notations.Integers]
_ is odd (Z_scope) [notation, in Waterproof.Notations.Integers]
_ is even (Z_scope) [notation, in Waterproof.Notations.Integers]
_ is divisible by _ (Z_scope) [notation, in Waterproof.Notations.Integers]
_ | _ (Z_scope) [notation, in Waterproof.Notations.Integers]
_ 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 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]
_ ? [notation, in Waterproof.Notations.Common]
_ ⟶ _ [notation, in Waterproof.Notations.Reals]
_ is empty [notation, in Waterproof.Notations.Sets]
_ ◦ _ ◦ _ [notation, in Waterproof.Libs.Analysis.SubsequencesMetric]
_ ◦ _ [notation, in Waterproof.Libs.Analysis.SubsequencesMetric]
_ 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.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: - We first define n_0 . [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: { Indeed, _ . } or write: { We need to verify that _ . } if intermediary proof steps are required. [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]
Fix an earlier warning [notation, in Waterproof.Util.Goals]
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]
subset _ [notation, in Waterproof.Notations.Sets]
the Archimedean property [notation, in Waterproof.Libs.Reals.ArchimedN]
_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]
Σ _ equals _ [notation, in Waterproof.Notations.Reals]
ℕ [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.IndexedSets]

Notation Index

Q

∃ _ .. _ , _ (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]

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]
< _ (chain_scope) [in Waterproof.Chains.Inequalities]
_ is an inverse of _ (function_scope) [in Waterproof.Notations.Functions]
_ has an inverse (function_scope) [in Waterproof.Notations.Functions]
_ is a right inverse of _ (function_scope) [in Waterproof.Notations.Functions]
_ has a right inverse (function_scope) [in Waterproof.Notations.Functions]
_ is a left inverse of _ (function_scope) [in Waterproof.Notations.Functions]
_ has a left inverse (function_scope) [in Waterproof.Notations.Functions]
_ is bijective (function_scope) [in Waterproof.Notations.Functions]
_ is surjective (function_scope) [in Waterproof.Notations.Functions]
_ is injective (function_scope) [in Waterproof.Notations.Functions]
_ ∘ _ (function_scope) [in Waterproof.Notations.Functions]
_ ⁻¹ [ _ ] (function_scope) [in Waterproof.Notations.Functions]
_ [ _ ] (function_scope) [in Waterproof.Notations.Functions]
_ 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]
index sequence (metric_scope) [in Waterproof.Libs.Analysis.SubsequencesMetric]
_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]
≠ _ (pred_for_subset_scope) [in Waterproof.Notations.Sets]
≥ _ (pred_for_subset_scope) [in Waterproof.Notations.Sets]
> _ (pred_for_subset_scope) [in Waterproof.Notations.Sets]
≤ _ (pred_for_subset_scope) [in Waterproof.Notations.Sets]
< _ (pred_for_subset_scope) [in Waterproof.Notations.Sets]
∈ _ (pred_for_subset_scope) [in Waterproof.Notations.Sets]
index sequence (pred_for_subset_scope) [in Waterproof.Libs.Analysis.SubsequencesMetric]
_index sequence_ (pred_for_subset_scope) [in Waterproof.Libs.Analysis.SubsequencesMetric]
_ is a single interval (R_scope) [in Waterproof.Notations.RealsWithSubsets]
[ _ , ∞ ) (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]
｜ _ - _ ｜ (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]
_ is irrational (R2_scope) [in Waterproof.Notations.RealsWithSubsets]
_ is rational (R2_scope) [in Waterproof.Notations.RealsWithSubsets]
ℚ (R2_scope) [in Waterproof.Notations.RealsWithSubsets]
ℤ (R2_scope) [in Waterproof.Notations.RealsWithSubsets]
∃! _ _ , _ (subset_scope) [in Waterproof.Notations.Sets]
{ _ , _ } (subset_scope) [in Waterproof.Notations.Sets]
{ _ ∈ _ | _ } (subset_scope) [in Waterproof.Notations.Sets]
for all _ _ , _ (subset_scope) [in Waterproof.Notations.Sets]
∀ _ _ , _ (subset_scope) [in Waterproof.Notations.Sets]
there exists _ _ , _ (subset_scope) [in Waterproof.Notations.Sets]
∃ _ _ , _ (subset_scope) [in Waterproof.Notations.Sets]
_ < _ (subset_scope) [in Waterproof.Notations.Sets]
_ ≤ _ (subset_scope) [in Waterproof.Notations.Sets]
_ > _ (subset_scope) [in Waterproof.Notations.Sets]
_ ≥ _ (subset_scope) [in Waterproof.Notations.Sets]
𝒫( _ ) (subset_scope) [in Waterproof.Notations.Sets]
[ _ ] (subset_scope) [in Waterproof.Notations.Sets]
｛ _ : _ | _ ｝ (subset_scope) [in Waterproof.Notations.Sets]
_ is inhabited (subset_scope) [in Waterproof.Notations.Sets]
_ is empty (subset_scope) [in Waterproof.Notations.Sets]
_ is disjoint from _ (subset_scope) [in Waterproof.Notations.Sets]
_ ⊂ _ (subset_scope) [in Waterproof.Notations.Sets]
_ ∉ _ (subset_scope) [in Waterproof.Notations.Sets]
_ \ _ (subset_scope) [in Waterproof.Notations.Sets]
_ ∪ _ (subset_scope) [in Waterproof.Notations.Sets]
_ ∩ _ (subset_scope) [in Waterproof.Notations.Sets]
Ω (subset_scope) [in Waterproof.Notations.Sets]
∅ (subset_scope) [in Waterproof.Notations.Sets]
⋂_{ _ _ } _ (subset_scope) [in Waterproof.Notations.IndexedSets]
_ ≠ _ (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]
_ ∨ _ (type_scope) [in Waterproof.Notations.Common]
fun _ .. _ ↦ _ (type_scope) [in Waterproof.Notations.Common]
_ ( _ , .. , _ ) (type_scope) [in Waterproof.Notations.Common]
for all _ , _ (type_scope) [in Waterproof.Notations.Sets]
∀ _ , _ (type_scope) [in Waterproof.Notations.Sets]
there exists _ , _ (type_scope) [in Waterproof.Notations.Sets]
∃ _ , _ (type_scope) [in Waterproof.Notations.Sets]
_ ∈ _ (type_scope) [in Waterproof.Notations.Sets]
_ ³ (Z_scope) [in Waterproof.Notations.Integers]
_ leaves a remainder of _ when divided by _ (Z_scope) [in Waterproof.Notations.Integers]
_ is a perfect square (Z_scope) [in Waterproof.Notations.Integers]
_ ² (Z_scope) [in Waterproof.Notations.Integers]
_ is odd (Z_scope) [in Waterproof.Notations.Integers]
_ is even (Z_scope) [in Waterproof.Notations.Integers]
_ is divisible by _ (Z_scope) [in Waterproof.Notations.Integers]
_ | _ (Z_scope) [in Waterproof.Notations.Integers]
_ 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 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]
_ ? [in Waterproof.Notations.Common]
_ ⟶ _ [in Waterproof.Notations.Reals]
_ is empty [in Waterproof.Notations.Sets]
_ ◦ _ ◦ _ [in Waterproof.Libs.Analysis.SubsequencesMetric]
_ ◦ _ [in Waterproof.Libs.Analysis.SubsequencesMetric]
_ 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.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: - We first define n_0 . [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: { Indeed, _ . } or write: { We need to verify that _ . } if intermediary proof steps are required. [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]
Fix an earlier warning [in Waterproof.Util.Goals]
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]
subset _ [in Waterproof.Notations.Sets]
the Archimedean property [in Waterproof.Libs.Reals.ArchimedN]
_limit_ of _ in _ is _ [in Waterproof.Libs.Analysis.ContinuityDomainR]
_limit_ of _ in _ is _ [in Waterproof.Libs.Analysis.ContinuityDomainNat]
& _ _ _ .. _ [in Waterproof.Chains.Inequalities]
Σ _ equals _ [in Waterproof.Notations.Reals]
ℕ [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.IndexedSets]

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]

Q

Quantifiers [in Waterproof.Notations.Common]

S

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

V

VerifyGoal [in Waterproof.Util.Goals]

Variable Index

C

Construction.A [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
Construction.a0 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
Construction.Hstep [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
Construction.HypP [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
Construction.H0 [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
Construction.P [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]

D

Definitions.X [in Waterproof.Libs.Analysis.MetricSpaces]

M

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

Library Index

A

Analysis
ArchimedN
Assertions
Assume
Automation

B

Because
Binders
BothDirections
BothStatements
BySince

C

Chains
Choose
Claims
Common
Conclusion
Constr
ConstructiveLogic
ContinuityDomainNat
ContinuityDomainR
Contradiction

D

Define
Divisibility

E

Either
Evars
Even

F

Functions
Functions

G

Goals

H

Help
Hints
Hypothesis

I

IndexedOperations
IndexedSets
Induction
Inequalities
InformativeEpsilon
Init
Integer
Integers
Integers
Intervals
ItHolds
ItSuffices

L

LimsupLiminfBolzano
Logic

M

Manipulation
MessagesToUser
MetricSpaces

N

Negation
Notations

O

Obtain
OpenAndClosed
Operations

Q

R

Rational
RealInequalities
Reals
Reals
RealsWithSubsets

S

Sequences
SequencesMetric
SequentialAccumulationPoints
Series
Sets
Sets
Specialize
Square
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]
alternative_char_unique_exists [in Waterproof.Libs.Logic.Quantification]
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]
archimedN [in Waterproof.Libs.Reals.ArchimedN]
archimedN_exists [in Waterproof.Libs.Reals.ArchimedN]
aux1 [in Waterproof.Libs.Analysis.ContinuityDomainNat]

B

bdd_below_to_bdd_above_set_opp [in Waterproof.Libs.Analysis.SupAndInf]
bdd_above_bound_iff [in Waterproof.Libs.Analysis.SupAndInf]
bijective_iff [in Waterproof.Libs.Functions]
bijective_is_surjective [in Waterproof.Libs.Functions]
bijective_is_injective [in Waterproof.Libs.Functions]
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_with_element_notation [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
classic_strong_ind_index_seq_with_prop [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
convergence_opp [in Waterproof.Libs.Analysis.Sequences]
convergence_minus [in Waterproof.Libs.Analysis.Sequences]
convergence_plus [in Waterproof.Libs.Analysis.Sequences]
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]
diff_is_rational [in Waterproof.Libs.Reals.Rational]
divide_char_inv [in Waterproof.Libs.Integers.Divisibility]
divide_char [in Waterproof.Libs.Integers.Divisibility]
div_is_rational [in Waterproof.Libs.Reals.Rational]
div_one_neq_zero [in Waterproof.Libs.Reals]
div_non_zero [in Waterproof.Libs.Reals]
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]
empty_set_characterization [in Waterproof.Libs.Sets]
equivalent_subsequence_convergence [in Waterproof.Libs.Analysis.SubsequencesMetric]
eq_seq_conv_to_same_lim [in Waterproof.Libs.Analysis.Sequences]
even_or_odd [in Waterproof.Libs.Integers.Even]
even_of [in Waterproof.Libs.Integers.Even]
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]
exists_exists_in_iff [in Waterproof.Notations.Sets]
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]
forall_forall_in_iff [in Waterproof.Notations.Sets]

G

ge_zero_gt_one [in Waterproof.Libs.Reals.Integer]

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_union_elim_left [in Waterproof.Libs.Sets.IndexedOperations]
index_union_elim [in Waterproof.Libs.Sets.IndexedOperations]
index_intersection_elim_left [in Waterproof.Libs.Sets.IndexedOperations]
index_intersection_elim [in Waterproof.Libs.Sets.IndexedOperations]
index_sequence_property2_automation [in Waterproof.Libs.Analysis.SubsequencesMetric]
index_sequence_property2 [in Waterproof.Libs.Analysis.SubsequencesMetric]
index_seq_equiv [in Waterproof.Libs.Analysis.SubsequencesMetric]
index_sequence_property_automation [in Waterproof.Libs.Analysis.SubsequencesMetric]
index_sequence_property [in Waterproof.Libs.Analysis.SubsequencesMetric]
induction_principle_elements [in Waterproof.Tactics.Induction]
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]
injective_elim [in Waterproof.Libs.Functions]
INR_0 [in Waterproof.Libs.Reals.Integer]
INR_1 [in Waterproof.Libs.Reals.Integer]
intersection_characterization_left [in Waterproof.Libs.Sets.Operations]
intersection_characterization [in Waterproof.Libs.Sets.Operations]
int_is_rational [in Waterproof.Libs.Reals.Rational]
inverse_intro [in Waterproof.Libs.Functions]
inverse_elim_right [in Waterproof.Libs.Functions]
inverse_elim_left [in Waterproof.Libs.Functions]
inverse_is_right_inverse [in Waterproof.Libs.Functions]
inverse_is_left_inverse [in Waterproof.Libs.Functions]
inv_remove [in Waterproof.Libs.Reals]
in_preimage_iff [in Waterproof.Libs.Functions]
in_preimage_elim [in Waterproof.Libs.Functions]
in_preimage_intro [in Waterproof.Libs.Functions]
in_image_iff [in Waterproof.Libs.Functions]
in_image_elim [in Waterproof.Libs.Functions]
in_image_intro [in Waterproof.Libs.Functions]
in_implies_not_in_compl [in Waterproof.Libs.Analysis.OpenAndClosed]
is_bounded_equivalence [in Waterproof.Libs.Analysis.Sequences]
is_sup_is_lub_iff [in Waterproof.Libs.Analysis.SupAndInf]
is_upper_bound_Raxioms_is_upper_bound_iff [in Waterproof.Libs.Analysis.SupAndInf]

L

left_inverse_intro [in Waterproof.Libs.Functions]
left_inverse_elim [in Waterproof.Libs.Functions]
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]
mem_of_preimage [in Waterproof.Libs.Functions]
mem_subset_full_set [in Waterproof.Notations.Sets]
minus_Z_in_R [in Waterproof.Libs.Reals.Integer]
min_1_over_n_plus_1_to_0 [in Waterproof.Libs.Analysis.Sequences]
min_frac [in Waterproof.Libs.Reals.Rational]
mouse_tail [in Waterproof.Libs.Analysis.Series]
mult_Z_in_R [in Waterproof.Libs.Reals.Integer]
mult_neq_zero [in Waterproof.Libs.Reals.RealInequalities]
mult_is_rational [in Waterproof.Libs.Reals.Rational]

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]
neg_Z_in_R [in Waterproof.Libs.Reals.Integer]
neg_is_rational [in Waterproof.Libs.Reals.Rational]
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_even_and_odd [in Waterproof.Libs.Integers.Even]
not_in_empty [in Waterproof.Libs.Sets]
not_in_compl_implies_in [in Waterproof.Libs.Analysis.OpenAndClosed]

O

odd_of [in Waterproof.Libs.Integers.Even]
one_Z_in_R [in Waterproof.Libs.Reals.Integer]
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]
perfect_square_of [in Waterproof.Libs.Integers.Square]
plus_Z_in_R [in Waterproof.Libs.Reals.Integer]
plus_frac [in Waterproof.Libs.Reals.Rational]
pos_not_neg_func [in Waterproof.Libs.Negation]
power_set_characterization_alt [in Waterproof.Libs.Sets]
power_set_characterization [in Waterproof.Libs.Sets]
preimage_of_mem [in Waterproof.Libs.Functions]

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]
rational_of [in Waterproof.Libs.Reals.Rational]
Rdivid_ineq_interchange [in Waterproof.Libs.Reals.RealInequalities]
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]
remainder_of [in Waterproof.Libs.Integers.Divisibility]
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_inverse_intro [in Waterproof.Libs.Functions]
right_inverse_elim [in Waterproof.Libs.Functions]
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_unsealed [in Waterproof.Libs.Analysis.SupAndInf]
R_complete [in Waterproof.Libs.Analysis.SupAndInf]

S

sequence_ub_bds [in Waterproof.Libs.Analysis.LimsupLiminfBolzano]
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]
seq_bdd_seq_acc_pts_bdd [in Waterproof.Libs.Analysis.SequentialAccumulationPoints]
set_difference_elim [in Waterproof.Libs.Sets]
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]
sum_is_rational [in Waterproof.Libs.Reals.Rational]
sup_is_upp_bd [in Waterproof.Libs.Analysis.SupAndInf]
sup_set_opp_is_inf_set [in Waterproof.Libs.Analysis.SupAndInf]
surjective_elim [in Waterproof.Libs.Functions]

T

true_Req [in Waterproof.Libs.Reals]
two_Z_in_R [in Waterproof.Libs.Reals.Integer]

U

union_characterization_left [in Waterproof.Libs.Sets.Operations]
union_characterization [in Waterproof.Libs.Sets.Operations]
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_Z_in_R [in Waterproof.Libs.Reals.Integer]
zero_in_interval_closed_zero_open_one [in Waterproof.Libs.Analysis.OpenAndClosed]
Zeven_char_inv [in Waterproof.Libs.Integers.Even]
Zeven_char [in Waterproof.Libs.Integers.Even]
Zodd_char_inv [in Waterproof.Libs.Integers.Even]
Zodd_char [in Waterproof.Libs.Integers.Even]

_

_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]
Closed [in Waterproof.Libs.Reals.Intervals]
Closed_Open [in Waterproof.Libs.Reals.Intervals]

I

index_union_intro [in Waterproof.Libs.Sets.IndexedOperations]
index_intersection_intro [in Waterproof.Libs.Sets.IndexedOperations]

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]

O

Open [in Waterproof.Libs.Reals.Intervals]
Open_Closed [in Waterproof.Libs.Reals.Intervals]

R

right [in Waterproof.Tactics.Either]

S

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

V

VerifyGoal.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]

F

fix_earlier_warning [in Waterproof.Util.Goals]

G

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

I

indexed_union [in Waterproof.Libs.Sets.IndexedOperations]
indexed_intersection [in Waterproof.Libs.Sets.IndexedOperations]
is_interval [in Waterproof.Libs.Reals.Intervals]

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.Base.Wrapper [in Waterproof.Util.Goals]
StrongIndIndxSeq.Step.Wrapper [in Waterproof.Util.Goals]
sumtriad [in Waterproof.Tactics.Either]

V

VerifyGoal.Wrapper [in Waterproof.Util.Goals]

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

ge_op [in Waterproof.Notations.Sets]
global_statement [in Waterproof.Chains.Inequalities]
grtr_rel_to_pred [in Waterproof.Chains.Inequalities]
gt_op [in Waterproof.Notations.Sets]

L

less_rel_to_pred [in Waterproof.Chains.Inequalities]
le_op [in Waterproof.Notations.Sets]
lt_op [in Waterproof.Notations.Sets]

N

ne_op [in Waterproof.Notations.Sets]

T

total_statement [in Waterproof.Chains.Inequalities]

W

weak_global_statement [in Waterproof.Chains.Inequalities]

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]

N

nat_ne_type [in Waterproof.Notations.Sets]
nat_lt_type [in Waterproof.Notations.Sets]
nat_le_type [in Waterproof.Notations.Sets]
nat_gt_type [in Waterproof.Notations.Sets]
nat_ge_type [in Waterproof.Notations.Sets]

O

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

R

R_ne_type [in Waterproof.Notations.Sets]
R_lt_type [in Waterproof.Notations.Sets]
R_le_type [in Waterproof.Notations.Sets]
R_gt_type [in Waterproof.Notations.Sets]
R_ge_type [in Waterproof.Notations.Sets]

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]

Abbreviation Index

P

partial_sums [in Waterproof.Libs.Analysis.Series]

Definition Index

A

as_subset [in Waterproof.Notations.Sets]
a_seq [in Waterproof.Libs.Analysis.Sequences]

B

bijective [in Waterproof.Libs.Functions]
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]
composition [in Waterproof.Libs.Functions]
constant_sequence [in Waterproof.Libs.Analysis.Sequences]
const_seq_from [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
const_seq [in Waterproof.Libs.Analysis.StrongInductionIndexSequence]
conv [in Waterproof.Notations.Sets]
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]
EqualChain_sind [in Waterproof.Chains.Inequalities]
EqualChain_rec [in Waterproof.Chains.Inequalities]
EqualChain_ind [in Waterproof.Chains.Inequalities]
EqualChain_rect [in Waterproof.Chains.Inequalities]
EqualRel_sind [in Waterproof.Chains.Inequalities]
EqualRel_rec [in Waterproof.Chains.Inequalities]
EqualRel_ind [in Waterproof.Chains.Inequalities]
EqualRel_rect [in Waterproof.Chains.Inequalities]
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]
fix_earlier_warning_sind [in Waterproof.Util.Goals]
fix_earlier_warning_rec [in Waterproof.Util.Goals]
fix_earlier_warning_ind [in Waterproof.Util.Goals]
fix_earlier_warning_rect [in Waterproof.Util.Goals]
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]
GreaterChain_sind [in Waterproof.Chains.Inequalities]
GreaterChain_rec [in Waterproof.Chains.Inequalities]
GreaterChain_ind [in Waterproof.Chains.Inequalities]
GreaterChain_rect [in Waterproof.Chains.Inequalities]
GreaterRel_sind [in Waterproof.Chains.Inequalities]
GreaterRel_rec [in Waterproof.Chains.Inequalities]
GreaterRel_ind [in Waterproof.Chains.Inequalities]
GreaterRel_rect [in Waterproof.Chains.Inequalities]
grtr_relation_flow [in Waterproof.Chains.Inequalities]

H

has_inverse [in Waterproof.Libs.Functions]
has_right_inverse [in Waterproof.Libs.Functions]
has_left_inverse [in Waterproof.Libs.Functions]

I

id [in Waterproof.Tactics.Specialize]
identity_seal [in Waterproof.Notations.Common]
image [in Waterproof.Libs.Functions]
indexed_union_sind [in Waterproof.Libs.Sets.IndexedOperations]
indexed_union_ind [in Waterproof.Libs.Sets.IndexedOperations]
indexed_intersection_sind [in Waterproof.Libs.Sets.IndexedOperations]
indexed_intersection_ind [in Waterproof.Libs.Sets.IndexedOperations]
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]
injective [in Waterproof.Libs.Functions]
inverse [in Waterproof.Libs.Functions]
is_square [in Waterproof.Libs.Integers.Square]
is_increasing [in Waterproof.Libs.Analysis.Subsequences]
is_index_seq [in Waterproof.Libs.Analysis.Subsequences]
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_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_sup [in Waterproof.Libs.Analysis.SupAndInf]
is_bounded_above [in Waterproof.Libs.Analysis.SupAndInf]
is_upper_bound [in Waterproof.Libs.Analysis.SupAndInf]
is_rational [in Waterproof.Libs.Reals.Rational]
is_seq_acc_pt [in Waterproof.Libs.Analysis.SequentialAccumulationPoints]
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_closed [in Waterproof.Libs.Analysis.OpenAndClosed]
is_open [in Waterproof.Libs.Analysis.OpenAndClosed]
is_interior_point [in Waterproof.Libs.Analysis.OpenAndClosed]
is_interval_sind [in Waterproof.Libs.Reals.Intervals]
is_interval_ind [in Waterproof.Libs.Reals.Intervals]
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]
left_inverse [in Waterproof.Libs.Functions]
LessChain_sind [in Waterproof.Chains.Inequalities]
LessChain_rec [in Waterproof.Chains.Inequalities]
LessChain_ind [in Waterproof.Chains.Inequalities]
LessChain_rect [in Waterproof.Chains.Inequalities]
LessRel_sind [in Waterproof.Chains.Inequalities]
LessRel_rec [in Waterproof.Chains.Inequalities]
LessRel_ind [in Waterproof.Chains.Inequalities]
LessRel_rect [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]

P

preimage [in Waterproof.Libs.Functions]

Q

Q_in_R [in Waterproof.Libs.Reals.Rational]

R

remainder [in Waterproof.Libs.Integers.Divisibility]
right_inverse [in Waterproof.Libs.Functions]

S

seal [in Waterproof.Notations.Sets]
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]
square [in Waterproof.Libs.Integers.Square]
StateGoal.unwrap [in Waterproof.Util.Goals]
StateHyp.unwrap [in Waterproof.Util.Goals]
StrongIndIndxSeq.Base.unwrap [in Waterproof.Util.Goals]
StrongIndIndxSeq.Step.unwrap [in Waterproof.Util.Goals]
subset_in [in Waterproof.Notations.Sets]
subset_type [in Waterproof.Notations.Sets]
sumtriad_sind [in Waterproof.Tactics.Either]
sumtriad_rec [in Waterproof.Tactics.Either]
sumtriad_ind [in Waterproof.Tactics.Either]
sumtriad_rect [in Waterproof.Tactics.Either]
surjective [in Waterproof.Libs.Functions]

T

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

U

unique_exists [in Waterproof.Notations.Sets]

V

VerifyGoal.unwrap [in Waterproof.Util.Goals]

Y

y_seq [in Waterproof.Libs.Analysis.Sequences]

Z

Z_in_R [in Waterproof.Libs.Reals.Integer]

Record Index

C

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

E

EqualInterpretation [in Waterproof.Chains.Inequalities]

G

ge_type [in Waterproof.Notations.Sets]
gt_type [in Waterproof.Notations.Sets]

I

InterpretableChain [in Waterproof.Chains.Inequalities]

L

le_type [in Waterproof.Notations.Sets]
lt_type [in Waterproof.Notations.Sets]

N

ne_type [in Waterproof.Notations.Sets]

O

OrderInterpretation [in Waterproof.Chains.Inequalities]

Global Index

J

K

X

(852 entries)

Notation Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

R

S

T

U

V

W

X

Y

Z

_

(188 entries)

Module Index

A

D

E

F

G

I

J

K

L

M

O

P

R

T

U

W

X

Y

Z

_

other

(13 entries)

Variable Index

A

B

E

F

G

H

I

J

K

L

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(9 entries)

Library Index

J

K

P

X

Y

Z

_

other

(79 entries)

Lemma Index

J

K

V

W

X

Y

other

(241 entries)

Constructor Index

A

D

E

F

G

H

J

K

P

Q

T

U

W

X

Y

Z

_

other

(35 entries)

Inductive Index

A

D

H

J

K

M

O

P

Q

R

T

U

W

X

Y

Z

_

other

(22 entries)

Projection Index

A

B

D

F

H

I

J

K

M

O

P

Q

R

S

U

V

X

Y

Z

_

other

(13 entries)

Instance Index

A

C

D

F

H

I

J

K

M

P

Q

S

T

U

V

W

X

Y

Z

_

other

(66 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)

Abbreviation Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

Q

R

S

T

U

V

W

X

Y

Z

_

other

(1 entry)

Definition Index

J

K

M

W

X

_

other

(169 entries)

Record Index

A

B

D

F

H

J

K

M

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(10 entries)

This page has been generated by coqdoc