Basic

📁 Source: Mathlib/Algebra/Order/CauSeq/Basic.lean

Statistics

Metric	Count
Definitions CauSeq, LimZero, Pos, addGroup, addGroupWithOne, const, equiv, instAdd, instCoeFunForallNat, instCommRingOfIsAbsoluteValue, instInhabited, instIntCast, instLEAbs, instLTAbs, instMaxAbs, instMinAbs, instMul, instNatCast, instNeg, instOne, instPowNat, instPreorderAbs, instSMul, instSub, instZero, inv, ofEq, IsCauSeq	28
Theorems abv_pos_of_not_limZero, add_apply, add_equiv_add, add_limZero, add_pos, bounded, bounded', cauchy, cauchy₂, cauchy₃, coe_add, coe_const, coe_inf, coe_inv, coe_mul, coe_neg, coe_one, coe_pow, coe_smul, coe_sub, coe_sup, coe_zero, const_add, const_apply, const_equiv, const_inj, const_inv, const_le, const_limZero, const_lt, const_mul, const_neg, const_one, const_pos, const_pow, const_smul, const_sub, const_zero, equiv_def₃, exists_gt, exists_lt, ext, ext_iff, inf_comm, inf_eq_left, inf_eq_right, inf_equiv_inf, inf_idem, inf_le_left, inf_le_right, inf_limZero, instIsScalarTower, inv_apply, inv_aux, inv_mul_cancel, isCauSeq, le_antisymm, le_inf, le_of_eq_of_le, le_of_exists, le_of_le_of_eq, le_sup_left, le_sup_right, le_total, limZero_congr, limZero_sub_rev, lt_inf, lt_irrefl, lt_of_eq_of_lt, lt_of_lt_of_eq, lt_total, lt_trans, mul_apply, mul_equiv_mul, mul_equiv_zero, mul_equiv_zero', mul_inv_cancel, mul_limZero_left, mul_limZero_right, mul_not_equiv_zero, mul_pos, neg_apply, neg_equiv_neg, neg_limZero, not_limZero_of_not_congr_zero, not_limZero_of_pos, of_near, one_apply, one_not_equiv_zero, pos_add_limZero, pow_apply, pow_equiv_pow, rat_inf_continuous_lemma, rat_sup_continuous_lemma, smul_apply, smul_equiv_smul, sub_apply, sub_equiv_sub, sub_limZero, sup_comm, sup_eq_left, sup_eq_right, sup_equiv_sup, sup_idem, sup_inf_distrib_left, sup_inf_distrib_right, sup_le, sup_limZero, sup_lt, trichotomy, zero_apply, zero_limZero, add, bounded, bounded', cauchy₂, cauchy₃, const, mul, neg, of_neg, isCauSeq_neg, rat_add_continuous_lemma, rat_inv_continuous_lemma, rat_mul_continuous_lemma	125
Total	153

CauSeq

Definitions

Name	Category	Theorems
LimZero 📖	MathDef	10 math math: not_limZero_of_pos, limZero_congr, const_limZero, lim_eq_zero_iff, PadicSeq.not_limZero_const_of_nonzero, not_limZero_of_not_congr_zero, Completion.mk_eq, Completion.mk_eq_zero, trichotomy, zero_limZero
Pos 📖	MathDef	3 math math: trichotomy, Real.mk_pos, const_pos
addGroup 📖	CompOp	—
addGroupWithOne 📖	CompOp	—
const 📖	CompOp	32 math math: const_one, IsComplete.isComplete, const_lt, lim_mul, Real.cauSeq_converges, const_neg, const_add, lim_const, const_limZero, PadicSeq.not_equiv_zero_const_of_nonzero, const_inj, const_apply, equiv_lim, const_mul, const_sub, const_equiv, const_le, PadicSeq.not_limZero_const_of_nonzero, exists_lt, Real.mk_const, one_not_equiv_zero, const_zero, coe_const, Complex.equiv_limAux, PadicSeq.norm_const, exists_gt, const_inv, const_pow, const_smul, Padic.const_equiv, complete, const_pos
equiv 📖	CompOp	31 math math: inv_mul_cancel, IsComplete.isComplete, Real.ofCauchy_sup, PadicSeq.ne_zero_iff_nequiv_zero, Real.cauSeq_converges, Padic.zero_def, Real.lt_cauchy, le_antisymm, sup_eq_right, sup_eq_left, PadicSeq.not_equiv_zero_const_of_nonzero, equiv_lim, PadicInt.nthHomSeq_mul, Padic.mk_eq, const_equiv, mul_inv_cancel, inf_eq_right, Completion.cau_seq_zero_ne_one, one_not_equiv_zero, Real.mk_eq, PadicInt.nthHomSeq_add, Complex.equiv_limAux, lt_total, PadicInt.nthHomSeq_one, Completion.mk_eq_mk, inf_eq_left, PadicSeq.norm_zero_iff, Padic.const_equiv, complete, PadicSeq.eq_zero_iff_equiv_zero, Real.ofCauchy_inf
instAdd 📖	CompOp	13 math math: const_add, lim_add, add_pos, PadicSeq.norm_nonarchimedean, Real.mk_add, Completion.mk_add, pos_add_limZero, coe_add, PadicSeq.add_eq_max_of_ne, PadicInt.nthHomSeq_add, add_limZero, add_apply, add_equiv_add
instCoeFunForallNat 📖	CompOp	—
instCommRingOfIsAbsoluteValue 📖	CompOp	—
instInhabited 📖	CompOp	—
instIntCast 📖	CompOp	—
instLEAbs 📖	CompOp	8 math math: le_of_exists, le_sup_left, const_le, inf_le_right, le_total, le_sup_right, Real.mk_le, inf_le_left
instLTAbs 📖	CompOp	7 math math: lt_irrefl, const_lt, Real.lt_cauchy, Real.mk_lt, exists_lt, lt_total, exists_gt
instMaxAbs 📖	CompOp	15 math math: sup_inf_distrib_right, Real.ofCauchy_sup, sup_idem, sup_lt, coe_sup, sup_equiv_sup, sup_eq_right, sup_eq_left, sup_limZero, le_sup_left, sup_le, sup_comm, le_sup_right, Real.mk_sup, sup_inf_distrib_left
instMinAbs 📖	CompOp	15 math math: sup_inf_distrib_right, inf_limZero, inf_comm, le_inf, inf_equiv_inf, inf_eq_right, inf_le_right, Real.mk_inf, lt_inf, inf_eq_left, sup_inf_distrib_left, inf_idem, coe_inf, inf_le_left, Real.ofCauchy_inf
instMul 📖	CompOp	19 math math: mul_equiv_mul, inv_mul_cancel, mul_apply, lim_mul, mul_pos, Real.mk_mul, mul_equiv_zero, PadicInt.nthHomSeq_mul, const_mul, mul_inv_cancel, mul_limZero_right, Completion.mk_mul, mul_not_equiv_zero, mul_equiv_zero', instIsScalarTower, mul_limZero_left, lim_mul_lim, PadicSeq.norm_mul, coe_mul
instNatCast 📖	CompOp	—
instNeg 📖	CompOp	10 math math: const_neg, PadicSeq.norm_neg, neg_limZero, neg_equiv_neg, neg_apply, lim_neg, coe_neg, Completion.mk_neg, Real.mk_neg, trichotomy
instOne 📖	CompOp	9 math math: const_one, inv_mul_cancel, one_apply, Real.mk_one, mul_inv_cancel, coe_one, Completion.cau_seq_zero_ne_one, PadicInt.nthHomSeq_one, PadicSeq.norm_one
instPowNat 📖	CompOp	5 math math: pow_equiv_pow, coe_pow, pow_apply, Completion.mk_pow, const_pow
instPreorderAbs 📖	CompOp	—
instSMul 📖	CompOp	6 math math: smul_apply, Completion.mk_smul, instIsScalarTower, smul_equiv_smul, const_smul, coe_smul
instSub 📖	CompOp	8 math math: sub_equiv_sub, sub_apply, sub_limZero, const_sub, lim_sub, coe_sub, Completion.mk_eq, Completion.mk_sub
instZero 📖	CompOp	11 math math: PadicSeq.ne_zero_iff_nequiv_zero, Padic.zero_def, zero_apply, PadicSeq.not_equiv_zero_const_of_nonzero, coe_zero, Completion.cau_seq_zero_ne_one, Real.mk_zero, const_zero, PadicSeq.norm_zero_iff, zero_limZero, PadicSeq.eq_zero_iff_equiv_zero
inv 📖	CompOp	7 math math: inv_mul_cancel, coe_inv, Completion.inv_mk, mul_inv_cancel, inv_apply, const_inv, lim_inv
ofEq 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
abv_pos_of_not_limZero 📖	mathematical	LimZero	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Preorder.toLE IsCauSeq	—	Nat.instAtLeastTwoHAddOfNat cauchy₃ half_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono lt_of_le_of_lt IsAbsoluteValue.abv_add add_lt_add IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add add_halves ZeroLEOneClass.neZero.two IsStrictOrderedRing.toZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero sub_add_cancel
add_apply 📖	mathematical	—	IsCauSeq CauSeq instAdd Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	—
add_equiv_add 📖	mathematical	CauSeq equiv	instAdd	—	add_limZero
add_limZero 📖	mathematical	LimZero	CauSeq instAdd	—	Nat.instAtLeastTwoHAddOfNat add_halves ZeroLEOneClass.neZero.two IsStrictOrderedRing.toZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing lt_of_le_of_lt IsAbsoluteValue.abv_add add_lt_add IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add exists_forall_ge_and half_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono
add_pos 📖	mathematical	Pos	CauSeq DivisionRing.toRing Field.toDivisionRing abs DistribLattice.toLattice instDistribLatticeOfLinearOrder AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne instAdd IsAbsoluteValue.abs_isAbsoluteValue	—	IsAbsoluteValue.abs_isAbsoluteValue exists_forall_ge_and add_pos IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing add_le_add covariant_swap_add_of_covariant_add
bounded 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsCauSeq	—	IsCauSeq.bounded
bounded' 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsCauSeq	—	IsCauSeq.bounded'
cauchy 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne IsCauSeq	—	—
cauchy₂ 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne IsCauSeq	—	IsCauSeq.cauchy₂
cauchy₃ 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne IsCauSeq	—	IsCauSeq.cauchy₃
coe_add 📖	mathematical	—	IsCauSeq CauSeq instAdd Pi.instAdd Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	—
coe_const 📖	mathematical	—	IsCauSeq const	—	—
coe_inf 📖	mathematical	—	IsCauSeq DivisionRing.toRing Field.toDivisionRing abs DistribLattice.toLattice instDistribLatticeOfLinearOrder AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CauSeq instMinAbs Pi.instMinForall_mathlib SemilatticeInf.toMin Lattice.toSemilatticeInf	—	—
coe_inv 📖	mathematical	LimZero DivisionRing.toRing	IsCauSeq inv Pi.instInv InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero DivisionRing.toDivisionSemiring	—	—
coe_mul 📖	mathematical	—	IsCauSeq CauSeq instMul Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	—
coe_neg 📖	mathematical	—	IsCauSeq CauSeq instNeg Pi.instNeg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup	—	—
coe_one 📖	mathematical	—	IsCauSeq CauSeq instOne Pi.instOne AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	—
coe_pow 📖	mathematical	—	IsCauSeq CauSeq instPowNat Pi.instPow Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring	—	—
coe_smul 📖	mathematical	—	IsCauSeq CauSeq instSMul Function.hasSMul	—	—
coe_sub 📖	mathematical	—	IsCauSeq CauSeq instSub Pi.instSub SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne	—	—
coe_sup 📖	mathematical	—	IsCauSeq DivisionRing.toRing Field.toDivisionRing abs DistribLattice.toLattice instDistribLatticeOfLinearOrder AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CauSeq instMaxAbs Pi.instMaxForall_mathlib SemilatticeSup.toMax Lattice.toSemilatticeSup	—	—
coe_zero 📖	mathematical	—	IsCauSeq CauSeq instZero Pi.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	—
const_add 📖	mathematical	—	const Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing CauSeq instAdd	—	—
const_apply 📖	mathematical	—	IsCauSeq const	—	—
const_equiv 📖	mathematical	—	CauSeq equiv const	—	const_sub const_limZero sub_eq_zero
const_inj 📖	mathematical	—	const	—	—
const_inv 📖	mathematical	—	const DivisionRing.toRing InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero DivisionRing.toDivisionSemiring inv	—	—
const_le 📖	mathematical	—	CauSeq DivisionRing.toRing Field.toDivisionRing abs DistribLattice.toLattice instDistribLatticeOfLinearOrder AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne instLEAbs const IsAbsoluteValue.abs_isAbsoluteValue Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf	—	IsAbsoluteValue.abs_isAbsoluteValue le_iff_lt_or_eq const_lt const_equiv
const_limZero 📖	mathematical	—	LimZero const MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	IsAbsoluteValue.abv_eq_zero eq_of_le_of_forall_lt_imp_le_of_dense LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono IsAbsoluteValue.abv_nonneg le_of_lt le_rfl zero_limZero
const_lt 📖	mathematical	—	CauSeq DivisionRing.toRing Field.toDivisionRing abs DistribLattice.toLattice instDistribLatticeOfLinearOrder AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne instLTAbs const IsAbsoluteValue.abs_isAbsoluteValue Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf	—	IsAbsoluteValue.abs_isAbsoluteValue const_sub const_pos sub_pos IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing
const_mul 📖	mathematical	—	const Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing CauSeq instMul	—	—
const_neg 📖	mathematical	—	const NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CauSeq instNeg	—	—
const_one 📖	mathematical	—	const AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CauSeq instOne	—	—
const_pos 📖	mathematical	—	Pos const DivisionRing.toRing Field.toDivisionRing abs DistribLattice.toLattice instDistribLatticeOfLinearOrder AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne IsAbsoluteValue.abs_isAbsoluteValue Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	—	IsAbsoluteValue.abs_isAbsoluteValue lt_of_lt_of_le le_rfl
const_pow 📖	mathematical	—	const Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring CauSeq instPowNat	—	—
const_smul 📖	mathematical	—	const CauSeq instSMul	—	—
const_sub 📖	mathematical	—	const SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CauSeq instSub	—	—
const_zero 📖	mathematical	—	const MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing CauSeq instZero	—	—
equiv_def₃ 📖	mathematical	CauSeq equiv Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne IsCauSeq	—	Nat.instAtLeastTwoHAddOfNat lt_of_le_of_lt IsAbsoluteValue.abv_add add_lt_add IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add add_halves ZeroLEOneClass.neZero.two IsStrictOrderedRing.toZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero sub_add_sub_cancel' exists_forall_ge_and half_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono cauchy₃
exists_gt 📖	mathematical	—	CauSeq DivisionRing.toRing Field.toDivisionRing abs DistribLattice.toLattice instDistribLatticeOfLinearOrder AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne instLTAbs const IsAbsoluteValue.abs_isAbsoluteValue	—	IsAbsoluteValue.abs_isAbsoluteValue bounded zero_lt_one IsStrictOrderedRing.toZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero sub_apply const_apply le_sub_iff_add_le' IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing add_le_add_iff_right covariant_swap_add_of_covariant_add IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT AddRightCancelSemigroup.toIsRightCancelAdd contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le le_of_lt abs_lt
exists_lt 📖	mathematical	—	CauSeq DivisionRing.toRing Field.toDivisionRing abs DistribLattice.toLattice instDistribLatticeOfLinearOrder AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne instLTAbs const IsAbsoluteValue.abs_isAbsoluteValue	—	IsAbsoluteValue.abs_isAbsoluteValue exists_gt const_neg sub_neg_eq_add add_comm
ext 📖	—	IsCauSeq	—	—	—
ext_iff 📖	mathematical	—	IsCauSeq	—	ext
inf_comm 📖	mathematical	—	CauSeq DivisionRing.toRing Field.toDivisionRing abs DistribLattice.toLattice instDistribLatticeOfLinearOrder AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne instMinAbs	—	inf_comm
inf_eq_left 📖	mathematical	CauSeq DivisionRing.toRing Field.toDivisionRing abs DistribLattice.toLattice instDistribLatticeOfLinearOrder AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne instLEAbs	equiv IsAbsoluteValue.abs_isAbsoluteValue instMinAbs	—	IsAbsoluteValue.abs_isAbsoluteValue inf_comm inf_eq_right
inf_eq_right 📖	mathematical	CauSeq DivisionRing.toRing Field.toDivisionRing abs DistribLattice.toLattice instDistribLatticeOfLinearOrder AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne instLEAbs	equiv IsAbsoluteValue.abs_isAbsoluteValue instMinAbs	—	IsAbsoluteValue.abs_isAbsoluteValue min_sub_sub_right IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing sub_self min_eq_right LE.le.trans LT.lt.le abs_zero IsOrderedAddMonoid.toAddLeftMono inf_equiv_inf inf_idem
inf_equiv_inf 📖	mathematical	CauSeq DivisionRing.toRing Field.toDivisionRing abs DistribLattice.toLattice instDistribLatticeOfLinearOrder AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne equiv IsAbsoluteValue.abs_isAbsoluteValue	instMinAbs	—	IsAbsoluteValue.abs_isAbsoluteValue LE.le.trans_lt abs_min_sub_min_le_max IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing max_lt sup_le_iff
inf_idem 📖	mathematical	—	CauSeq DivisionRing.toRing Field.toDivisionRing abs DistribLattice.toLattice instDistribLatticeOfLinearOrder AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne instMinAbs	—	inf_idem
inf_le_left 📖	mathematical	—	CauSeq DivisionRing.toRing Field.toDivisionRing abs DistribLattice.toLattice instDistribLatticeOfLinearOrder AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne instLEAbs instMinAbs	—	le_of_exists inf_le_left
inf_le_right 📖	mathematical	—	CauSeq DivisionRing.toRing Field.toDivisionRing abs DistribLattice.toLattice instDistribLatticeOfLinearOrder AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne instLEAbs instMinAbs	—	le_of_exists inf_le_right
inf_limZero 📖	mathematical	LimZero DivisionRing.toRing Field.toDivisionRing abs DistribLattice.toLattice instDistribLatticeOfLinearOrder AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne	CauSeq instMinAbs	—	abs_lt IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing covariant_swap_add_of_covariant_add lt_inf_iff inf_lt_iff exists_forall_ge_and
instIsScalarTower 📖	mathematical	—	IsScalarTower CauSeq instSMul instMul	—	smul_assoc Pi.isScalarTower'
inv_apply 📖	mathematical	LimZero DivisionRing.toRing	IsCauSeq inv InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero DivisionRing.toDivisionSemiring	—	—
inv_aux 📖	mathematical	LimZero DivisionRing.toRing Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero DivisionRing.toDivisionSemiring IsCauSeq	—	abv_pos_of_not_limZero rat_inv_continuous_lemma exists_forall_ge_and cauchy₃ le_rfl
inv_mul_cancel 📖	mathematical	LimZero DivisionRing.toRing	CauSeq equiv instMul inv instOne	—	abv_pos_of_not_limZero inv_mul_cancel₀ IsAbsoluteValue.abv_pos lt_of_lt_of_le sub_self IsAbsoluteValue.abv_zero
isCauSeq 📖	mathematical	—	IsCauSeq	—	—
le_antisymm 📖	mathematical	CauSeq DivisionRing.toRing Field.toDivisionRing abs DistribLattice.toLattice instDistribLatticeOfLinearOrder AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne instLEAbs	equiv IsAbsoluteValue.abs_isAbsoluteValue	—	not_lt_of_ge
le_inf 📖	mathematical	CauSeq DivisionRing.toRing Field.toDivisionRing abs DistribLattice.toLattice instDistribLatticeOfLinearOrder AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne instLEAbs	instMinAbs	—	lt_inf le_of_eq_of_le IsAbsoluteValue.abs_isAbsoluteValue LT.lt.le inf_eq_right inf_eq_left
le_of_eq_of_le 📖	—	CauSeq DivisionRing.toRing Field.toDivisionRing abs DistribLattice.toLattice instDistribLatticeOfLinearOrder AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne equiv IsAbsoluteValue.abs_isAbsoluteValue instLEAbs	—	—	IsAbsoluteValue.abs_isAbsoluteValue lt_of_eq_of_lt
le_of_exists 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsCauSeq DivisionRing.toRing Field.toDivisionRing abs AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne	CauSeq instLEAbs	—	IsAbsoluteValue.abs_isAbsoluteValue lt_total not_lt_of_ge le_max_left sub_pos IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing lt_of_lt_of_le le_max_right
le_of_le_of_eq 📖	—	CauSeq DivisionRing.toRing Field.toDivisionRing abs DistribLattice.toLattice instDistribLatticeOfLinearOrder AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne instLEAbs equiv IsAbsoluteValue.abs_isAbsoluteValue	—	—	IsAbsoluteValue.abs_isAbsoluteValue lt_of_lt_of_eq
le_sup_left 📖	mathematical	—	CauSeq DivisionRing.toRing Field.toDivisionRing abs DistribLattice.toLattice instDistribLatticeOfLinearOrder AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne instLEAbs instMaxAbs	—	le_of_exists le_sup_left
le_sup_right 📖	mathematical	—	CauSeq DivisionRing.toRing Field.toDivisionRing abs DistribLattice.toLattice instDistribLatticeOfLinearOrder AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne instLEAbs instMaxAbs	—	le_of_exists le_sup_right
le_total 📖	mathematical	—	CauSeq DivisionRing.toRing Field.toDivisionRing abs DistribLattice.toLattice instDistribLatticeOfLinearOrder AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne instLEAbs	—	IsAbsoluteValue.abs_isAbsoluteValue lt_total
limZero_congr 📖	mathematical	CauSeq equiv	LimZero	—	sub_add_cancel add_limZero
limZero_sub_rev 📖	—	LimZero CauSeq instSub	—	—	neg_sub neg_limZero
lt_inf 📖	mathematical	CauSeq DivisionRing.toRing Field.toDivisionRing abs DistribLattice.toLattice instDistribLatticeOfLinearOrder AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne instLTAbs	instMinAbs	—	lt_inf_iff min_le_min sup_le_iff LE.le.trans_eq min_sub_sub_right IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing
lt_irrefl 📖	mathematical	—	CauSeq DivisionRing.toRing Field.toDivisionRing abs DistribLattice.toLattice instDistribLatticeOfLinearOrder AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne instLTAbs	—	not_limZero_of_pos IsAbsoluteValue.abs_isAbsoluteValue sub_self
lt_of_eq_of_lt 📖	—	CauSeq DivisionRing.toRing Field.toDivisionRing abs DistribLattice.toLattice instDistribLatticeOfLinearOrder AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne equiv IsAbsoluteValue.abs_isAbsoluteValue instLTAbs	—	—	IsAbsoluteValue.abs_isAbsoluteValue pos_add_limZero neg_limZero sub_sub_sub_cancel_right sub_eq_add_neg
lt_of_lt_of_eq 📖	—	CauSeq DivisionRing.toRing Field.toDivisionRing abs DistribLattice.toLattice instDistribLatticeOfLinearOrder AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne instLTAbs equiv IsAbsoluteValue.abs_isAbsoluteValue	—	—	IsAbsoluteValue.abs_isAbsoluteValue neg_sub sub_add_sub_cancel' pos_add_limZero neg_limZero
lt_total 📖	mathematical	—	CauSeq DivisionRing.toRing Field.toDivisionRing abs DistribLattice.toLattice instDistribLatticeOfLinearOrder AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne instLTAbs equiv IsAbsoluteValue.abs_isAbsoluteValue	—	IsAbsoluteValue.abs_isAbsoluteValue neg_sub trichotomy
lt_trans 📖	—	CauSeq DivisionRing.toRing Field.toDivisionRing abs DistribLattice.toLattice instDistribLatticeOfLinearOrder AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne instLTAbs	—	—	IsAbsoluteValue.abs_isAbsoluteValue sub_add_sub_cancel' add_pos
mul_apply 📖	mathematical	—	IsCauSeq CauSeq instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	—
mul_equiv_mul 📖	mathematical	CauSeq equiv	instMul	—	sub_mul mul_sub sub_add_sub_cancel add_limZero mul_limZero_left mul_limZero_right
mul_equiv_zero 📖	mathematical	CauSeq equiv instZero	instMul	—	mul_limZero_right sub_zero
mul_equiv_zero' 📖	mathematical	CauSeq equiv instZero	instMul	—	mul_limZero_left sub_zero
mul_inv_cancel 📖	mathematical	LimZero DivisionRing.toRing	CauSeq equiv instMul inv instOne	—	abv_pos_of_not_limZero mul_inv_cancel₀ IsAbsoluteValue.abv_pos lt_of_lt_of_le sub_self IsAbsoluteValue.abv_zero
mul_limZero_left 📖	mathematical	LimZero	CauSeq instMul	—	bounded' mul_lt_mul'' IsStrictOrderedRing.toPosMulStrictMono IsOrderedRing.toMulPosMono IsStrictOrderedRing.toIsOrderedRing IsAbsoluteValue.abv_nonneg IsAbsoluteValue.abv_mul div_mul_cancel₀ ne_of_gt div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE
mul_limZero_right 📖	mathematical	LimZero	CauSeq instMul	—	bounded' mul_lt_mul' IsStrictOrderedRing.toPosMulStrictMono IsOrderedRing.toMulPosMono IsStrictOrderedRing.toIsOrderedRing le_of_lt IsAbsoluteValue.abv_nonneg IsAbsoluteValue.abv_mul div_mul_cancel₀ ne_of_gt mul_comm div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE
mul_not_equiv_zero 📖	mathematical	CauSeq equiv instZero	instMul	—	sub_zero abv_pos_of_not_limZero mul_pos IsStrictOrderedRing.toPosMulStrictMono le_max_left le_trans le_max_right not_le_of_gt IsAbsoluteValue.abv_mul mul_le_mul IsOrderedRing.toPosMulMono IsStrictOrderedRing.toIsOrderedRing IsOrderedRing.toMulPosMono le_of_lt IsAbsoluteValue.abv_nonneg
mul_pos 📖	mathematical	Pos	CauSeq DivisionRing.toRing Field.toDivisionRing abs DistribLattice.toLattice instDistribLatticeOfLinearOrder AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne instMul IsAbsoluteValue.abs_isAbsoluteValue	—	IsAbsoluteValue.abs_isAbsoluteValue exists_forall_ge_and mul_pos IsStrictOrderedRing.toPosMulStrictMono mul_le_mul IsOrderedRing.toPosMulMono IsStrictOrderedRing.toIsOrderedRing IsOrderedRing.toMulPosMono le_of_lt le_trans
neg_apply 📖	mathematical	—	IsCauSeq CauSeq instNeg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup	—	—
neg_equiv_neg 📖	mathematical	CauSeq equiv	instNeg	—	neg_sub' neg_limZero
neg_limZero 📖	mathematical	LimZero	CauSeq instNeg	—	neg_one_mul mul_limZero_right
not_limZero_of_not_congr_zero 📖	mathematical	CauSeq equiv instZero	LimZero	—	sub_zero
not_limZero_of_pos 📖	mathematical	Pos	LimZero DivisionRing.toRing Field.toDivisionRing abs DistribLattice.toLattice instDistribLatticeOfLinearOrder AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne	—	exists_forall_ge_and le_rfl not_lt_of_ge abs_lt IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing covariant_swap_add_of_covariant_add
of_near 📖	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne IsCauSeq	—	—	Nat.instAtLeastTwoHAddOfNat exists_forall_ge_and half_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono cauchy₃ le_rfl lt_of_le_of_lt IsAbsoluteValue.abv_add add_lt_add IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsAbsoluteValue.abv_sub IsDomain.to_noZeroDivisors Field.isDomain sub_add_sub_cancel add_right_comm add_halves ZeroLEOneClass.neZero.two IsStrictOrderedRing.toZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero
one_apply 📖	mathematical	—	IsCauSeq CauSeq instOne AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	—
one_not_equiv_zero 📖	mathematical	—	CauSeq equiv const AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	le_of_not_gt lt_irrefl sub_zero le_rfl IsAbsoluteValue.abv_nonneg le_antisymm IsAbsoluteValue.abv_eq_zero one_ne_zero NeZero.one IsDomain.toNontrivial
pos_add_limZero 📖	mathematical	Pos LimZero DivisionRing.toRing Field.toDivisionRing abs DistribLattice.toLattice instDistribLatticeOfLinearOrder AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne	CauSeq instAdd IsAbsoluteValue.abs_isAbsoluteValue	—	IsAbsoluteValue.abs_isAbsoluteValue Nat.instAtLeastTwoHAddOfNat exists_forall_ge_and half_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono add_le_add IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing covariant_swap_add_of_covariant_add le_of_lt abs_lt sub_self_div_two sub_eq_add_neg
pow_apply 📖	mathematical	—	IsCauSeq CauSeq instPowNat Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring	—	—
pow_equiv_pow 📖	mathematical	CauSeq equiv	instPowNat	—	pow_zero pow_succ' mul_equiv_mul
rat_inf_continuous_lemma 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder abs AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing SubNegMonoid.toSub AddGroup.toSubNegMonoid	SemilatticeInf.toMin	—	LE.le.trans_lt abs_min_sub_min_le_max IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing max_lt
rat_sup_continuous_lemma 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder abs AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing SubNegMonoid.toSub AddGroup.toSubNegMonoid	SemilatticeSup.toMax Lattice.toSemilatticeSup	—	LE.le.trans_lt abs_max_sub_max_le_max IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing max_lt
smul_apply 📖	mathematical	—	IsCauSeq CauSeq instSMul	—	—
smul_equiv_smul 📖	mathematical	CauSeq equiv	instSMul	—	smul_one_mul instIsScalarTower mul_equiv_mul const_equiv
sub_apply 📖	mathematical	—	IsCauSeq CauSeq instSub SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne	—	—
sub_equiv_sub 📖	mathematical	CauSeq equiv	instSub	—	sub_eq_add_neg add_equiv_add neg_equiv_neg
sub_limZero 📖	mathematical	LimZero	CauSeq instSub	—	sub_eq_add_neg add_limZero neg_limZero
sup_comm 📖	mathematical	—	CauSeq DivisionRing.toRing Field.toDivisionRing abs DistribLattice.toLattice instDistribLatticeOfLinearOrder AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne instMaxAbs	—	sup_comm
sup_eq_left 📖	mathematical	CauSeq DivisionRing.toRing Field.toDivisionRing abs DistribLattice.toLattice instDistribLatticeOfLinearOrder AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne instLEAbs	equiv IsAbsoluteValue.abs_isAbsoluteValue instMaxAbs	—	IsAbsoluteValue.abs_isAbsoluteValue sup_comm sup_eq_right
sup_eq_right 📖	mathematical	CauSeq DivisionRing.toRing Field.toDivisionRing abs DistribLattice.toLattice instDistribLatticeOfLinearOrder AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne instLEAbs	equiv IsAbsoluteValue.abs_isAbsoluteValue instMaxAbs	—	IsAbsoluteValue.abs_isAbsoluteValue max_sub_sub_right IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing sub_self max_eq_right sub_nonpos covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono sub_nonneg LE.le.trans LT.lt.le abs_zero sup_equiv_sup sup_idem
sup_equiv_sup 📖	mathematical	CauSeq DivisionRing.toRing Field.toDivisionRing abs DistribLattice.toLattice instDistribLatticeOfLinearOrder AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne equiv IsAbsoluteValue.abs_isAbsoluteValue	instMaxAbs	—	IsAbsoluteValue.abs_isAbsoluteValue LE.le.trans_lt abs_max_sub_max_le_max IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing max_lt sup_le_iff
sup_idem 📖	mathematical	—	CauSeq DivisionRing.toRing Field.toDivisionRing abs DistribLattice.toLattice instDistribLatticeOfLinearOrder AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne instMaxAbs	—	sup_idem
sup_inf_distrib_left 📖	mathematical	—	CauSeq DivisionRing.toRing Field.toDivisionRing abs DistribLattice.toLattice instDistribLatticeOfLinearOrder AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne instMaxAbs instMinAbs	—	ext max_min_distrib_left
sup_inf_distrib_right 📖	mathematical	—	CauSeq DivisionRing.toRing Field.toDivisionRing abs DistribLattice.toLattice instDistribLatticeOfLinearOrder AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne instMaxAbs instMinAbs	—	ext max_min_distrib_right
sup_le 📖	mathematical	CauSeq DivisionRing.toRing Field.toDivisionRing abs DistribLattice.toLattice instDistribLatticeOfLinearOrder AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne instLEAbs	instMaxAbs	—	sup_lt le_of_le_of_eq LT.lt.le IsAbsoluteValue.abs_isAbsoluteValue sup_eq_right sup_eq_left
sup_limZero 📖	mathematical	LimZero DivisionRing.toRing Field.toDivisionRing abs DistribLattice.toLattice instDistribLatticeOfLinearOrder AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne	CauSeq instMaxAbs	—	abs_lt IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing covariant_swap_add_of_covariant_add lt_sup_iff sup_lt_iff exists_forall_ge_and
sup_lt 📖	mathematical	CauSeq DivisionRing.toRing Field.toDivisionRing abs DistribLattice.toLattice instDistribLatticeOfLinearOrder AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne instLTAbs	instMaxAbs	—	lt_inf_iff min_le_min sup_le_iff LE.le.trans_eq min_sub_sub_left IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing
trichotomy 📖	mathematical	—	Pos LimZero DivisionRing.toRing Field.toDivisionRing abs DistribLattice.toLattice instDistribLatticeOfLinearOrder AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CauSeq instNeg IsAbsoluteValue.abs_isAbsoluteValue	—	IsAbsoluteValue.abs_isAbsoluteValue abv_pos_of_not_limZero exists_forall_ge_and cauchy₃ le_rfl abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing le_add_iff_nonneg_right IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le le_trans neg_le_sub_iff_le_add' le_of_lt abs_lt covariant_swap_add_of_covariant_add abs_of_nonpos sub_le_sub_iff_right zero_sub le_total
zero_apply 📖	mathematical	—	IsCauSeq CauSeq instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	—
zero_limZero 📖	mathematical	—	LimZero CauSeq instZero	—	IsAbsoluteValue.abv_zero

IsCauSeq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add 📖	mathematical	IsCauSeq	Pi.instAdd Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	rat_add_continuous_lemma exists_forall_ge_and cauchy₃ le_rfl
bounded 📖	mathematical	IsCauSeq	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	zero_lt_one IsStrictOrderedRing.toZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero Nat.instCanonicallyOrderedAdd LE.le.trans le_max_left le_total LE.le.trans_lt lt_add_one IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing add_sub_cancel IsAbsoluteValue.abv_add add_lt_add_of_le_of_lt covariant_swap_add_of_covariant_add le_rfl
bounded' 📖	mathematical	IsCauSeq	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	bounded LT.lt.trans_le lt_add_one IsStrictOrderedRing.toZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing le_max_right le_max_left
cauchy₂ 📖	mathematical	IsCauSeq Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne	—	Nat.instAtLeastTwoHAddOfNat add_halves ZeroLEOneClass.neZero.two IsStrictOrderedRing.toZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing lt_of_le_of_lt IsAbsoluteValue.abv_sub_le add_lt_add IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsAbsoluteValue.abv_sub IsDomain.to_noZeroDivisors Field.isDomain half_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono
cauchy₃ 📖	mathematical	IsCauSeq Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne	—	cauchy₂ le_trans
const 📖	mathematical	—	IsCauSeq	—	sub_self IsAbsoluteValue.abv_zero
mul 📖	mathematical	IsCauSeq	Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	bounded' rat_mul_continuous_lemma exists_forall_ge_and cauchy₃ le_rfl
neg 📖	mathematical	IsCauSeq	Pi.instNeg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup	—	isCauSeq_neg
of_neg 📖	—	IsCauSeq Pi.instNeg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup	—	—	isCauSeq_neg

(root)

Definitions

Name	Category	Theorems
CauSeq 📖	CompOp	96 math math: CauSeq.const_one, CauSeq.inv_mul_cancel, CauSeq.lt_irrefl, CauSeq.IsComplete.isComplete, CauSeq.sup_inf_distrib_right, Real.ofCauchy_sup, CauSeq.sup_idem, CauSeq.mul_apply, CauSeq.inf_limZero, CauSeq.const_lt, CauSeq.lim_mul, CauSeq.inf_comm, CauSeq.one_apply, Real.cauSeq_converges, CauSeq.const_neg, Padic.zero_def, Real.mk_one, CauSeq.coe_sup, CauSeq.mul_pos, CauSeq.const_add, CauSeq.lim_add, Real.lt_cauchy, CauSeq.add_pos, CauSeq.sub_apply, Real.mk_lt, CauSeq.sub_limZero, CauSeq.smul_apply, CauSeq.zero_apply, Real.mk_mul, PadicSeq.not_equiv_zero_const_of_nonzero, Real.mk_add, CauSeq.sup_limZero, CauSeq.equiv_lim, CauSeq.Completion.mk_smul, CauSeq.coe_zero, CauSeq.le_of_exists, CauSeq.Completion.mk_add, CauSeq.le_sup_left, CauSeq.const_mul, CauSeq.const_sub, CauSeq.const_equiv, CauSeq.const_le, CauSeq.lim_sub, CauSeq.mul_inv_cancel, CauSeq.sup_comm, CauSeq.pos_add_limZero, CauSeq.coe_one, CauSeq.mul_limZero_right, CauSeq.coe_sub, CauSeq.inf_le_right, CauSeq.Completion.mk_mul, CauSeq.exists_lt, CauSeq.Completion.cau_seq_zero_ne_one, CauSeq.coe_pow, CauSeq.one_not_equiv_zero, Real.mk_zero, CauSeq.pow_apply, CauSeq.le_total, CauSeq.coe_add, CauSeq.neg_limZero, CauSeq.le_sup_right, Real.mk_inf, CauSeq.const_zero, Real.mk_eq, Real.mk_sup, CauSeq.instIsScalarTower, CauSeq.Completion.mk_eq, Complex.equiv_limAux, CauSeq.neg_apply, CauSeq.lim_neg, CauSeq.lt_total, CauSeq.mul_limZero_left, CauSeq.add_limZero, CauSeq.coe_neg, CauSeq.Completion.mk_neg, CauSeq.Completion.mk_eq_mk, CauSeq.exists_gt, Real.mk_neg, CauSeq.trichotomy, CauSeq.Completion.mk_pow, CauSeq.Completion.mk_sub, CauSeq.add_apply, CauSeq.const_pow, CauSeq.sup_inf_distrib_left, CauSeq.inf_idem, CauSeq.lim_mul_lim, CauSeq.const_smul, Padic.const_equiv, Real.mk_le, CauSeq.complete, CauSeq.coe_smul, CauSeq.zero_limZero, CauSeq.coe_inf, CauSeq.inf_le_left, Real.ofCauchy_inf, CauSeq.coe_mul
IsCauSeq 📖	MathDef	64 math math: PadicInt.isCauSeq_nthHom, CauSeq.inv_aux, Padic.complete', IsCauSeq.of_decreasing_bounded, CauSeq.abv_pos_of_not_limZero, CauSeq.cauchy₂, CauSeq.mul_apply, CauSeq.ext_iff, Complex.isCauSeq_conj, Padic.exi_rat_seq_conv_cauchy, CauSeq.one_apply, IsCauSeq.const, Real.of_near, CauSeq.cauchy, CauSeq.coe_sup, PadicSeq.lift_index_left_left, CauSeq.bounded', padicNormE.defn, CauSeq.sub_apply, PadicSeq.lift_index_right, CauSeq.isCauSeq, CauSeq.smul_apply, CauSeq.zero_apply, Complex.isCauSeq_norm_exp, CauSeq.coe_inv, IsCauSeq.geo_series, CauSeq.const_apply, CauSeq.coe_zero, Padic.complete'', CauSeq.tendsto_limit, RCLike.isCauSeq_im, CauSeq.cauchySeq, Padic.exi_rat_seq_conv, CauSeq.coe_one, isCauSeq_iff_cauchySeq, CauSeq.coe_sub, PadicSeq.stationaryPoint_spec, CauSeq.coe_pow, CauSeq.pow_apply, PadicSeq.lift_index_left, CauSeq.inv_apply, CauSeq.coe_add, Complex.isCauSeq_im, PadicInt.isCauSeq_padicNorm_of_pow_dvd_sub, IsCauSeq.geo_series_const, CauSeq.coe_const, CauSeq.neg_apply, CauSeq.coe_neg, CauSeq.equiv_def₃, isCauSeq_neg, CauSeq.add_apply, IsCauSeq.of_mono_bounded, PadicSeq.stationary, CauchySeq.isCauSeq, Complex.isCauSeq_exp, RCLike.isCauSeq_re, CauSeq.bounded, Complex.isCauSeq_re, Real.isCauSeq_iff_lift, CauSeq.coe_smul, CauSeq.coe_inf, CauSeq.cauchy₃, IsCauSeq.series_ratio_test, CauSeq.coe_mul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isCauSeq_neg 📖	mathematical	—	IsCauSeq Pi.instNeg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup	—	IsAbsoluteValue.abv_neg IsStrictOrderedRing.toIsOrderedRing IsDomain.to_noZeroDivisors Field.isDomain
rat_add_continuous_lemma 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	Nat.instAtLeastTwoHAddOfNat half_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono sub_eq_add_neg neg_add_rev add_comm add_assoc add_left_comm add_halves ZeroLEOneClass.neZero.two IsStrictOrderedRing.toZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing lt_of_le_of_lt IsAbsoluteValue.abv_add add_lt_add IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add
rat_inv_continuous_lemma 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero DivisionRing.toDivisionSemiring	—	mul_pos IsStrictOrderedRing.toPosMulStrictMono LT.lt.trans_le inv_sub_inv' IsAbsoluteValue.abv_pos IsAbsoluteValue.abv_mul IsAbsoluteValue.abv_inv IsAbsoluteValue.abv_sub IsStrictOrderedRing.toIsOrderedRing IsDomain.to_noZeroDivisors Field.isDomain lt_of_mul_lt_mul_left PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE lt_of_mul_lt_mul_right MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono mul_assoc inv_mul_cancel_right₀ LT.lt.ne' mul_inv_cancel₀ one_mul mul_le_mul IsOrderedRing.toPosMulMono IsOrderedRing.toMulPosMono mul_le_mul_of_nonneg_right le_of_lt mul_nonneg LT.lt.le
rat_mul_continuous_lemma 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	lt_of_lt_of_le zero_lt_one IsStrictOrderedRing.toZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero le_max_left Nat.instAtLeastTwoHAddOfNat div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono half_pos le_trans le_max_right add_lt_add_of_lt_of_lt IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add mul_lt_mul'' IsOrderedRing.toMulPosMono IsAbsoluteValue.abv_nonneg sub_eq_add_neg add_mul Distrib.rightDistribClass neg_mul mul_add Distrib.leftDistribClass mul_neg add_left_comm add_neg_cancel_comm lt_of_le_of_lt IsAbsoluteValue.abv_add add_halves ZeroLEOneClass.neZero.two IsAbsoluteValue.abv_mul div_mul_cancel₀ ne_of_gt mul_comm

---

← Back to Index