Hyperreal

📁 Source: Mathlib/Analysis/Real/Hyperreal.lean

Statistics

Metric	Count
Definitions `InfiniteNeg`, `InfinitePos`, `Infinitesimal`, `IsSt`, `coeRingHom`, `epsilon`, `instCoeTCReal`, `instField`, `instLinearOrder`, `ofReal`, `ofSeq`, `omega`, `st`, `termε`, `termω`, `«termℝ*»`	16
Theorems `mul`, `ne_real`, `ne_zero`, `not_infinitesimal`, `st_eq`, `lt_zero`, `neg`, `not_infinitePos`, `not_infinitesimal`, `neg`, `not_infiniteNeg`, `not_infinitesimal`, `pos`, `add`, `eq_zero`, `mul`, `neg`, `not_infinite`, `add`, `infinitesimal_sub`, `inv`, `isSt_st`, `le`, `lt`, `map`, `map₂`, `mul`, `neg`, `not_infinite`, `st_eq`, `sub`, `unique`, `abs_lt_real_iff_infinitesimal`, `abs_omega`, `archimdeanClassMk_coe`, `archimedeanClassMk_coe_nonneg`, `archimedeanClassMk_epsilon_pos`, `archimedeanClassMk_neg_of_tendsto_atBot`, `archimedeanClassMk_neg_of_tendsto_atTop`, `archimedeanClassMk_nonneg_of_tendsto`, `archimedeanClassMk_omega_neg`, `archimedeanClassMk_pos_of_tendsto`, `coeRingHom_toFun`, `coe_abs`, `coe_add`, `coe_div`, `coe_eq_coe`, `coe_eq_one`, `coe_eq_zero`, `coe_inv`, `coe_le_coe`, `coe_lt_coe`, `coe_lt_omega`, `coe_max`, `coe_min`, `coe_mul`, `coe_ne_coe`, `coe_ne_one`, `coe_ne_zero`, `coe_neg`, `coe_nonneg`, `coe_ofNat`, `coe_one`, `coe_pos`, `coe_sub`, `coe_zero`, `epsilon_lt_of_neg`, `epsilon_lt_of_pos`, `epsilon_lt_pos`, `epsilon_mul_omega`, `epsilon_ne_zero`, `epsilon_pos`, `eq_of_isSt_real`, `exists_st_iff_not_infinite`, `exists_st_of_not_infinite`, `gt_of_neg_of_infinitesimal`, `gt_of_tendsto_zero_of_neg`, `infiniteNeg_add_infiniteNeg`, `infiniteNeg_add_not_infinite`, `infiniteNeg_add_not_infinitePos`, `infiniteNeg_def`, `infiniteNeg_iff_infinite_and_neg`, `infiniteNeg_iff_infinite_of_neg`, `infiniteNeg_iff_infinitesimal_inv_neg`, `infiniteNeg_mul_infiniteNeg`, `infiniteNeg_mul_infinitePos`, `infiniteNeg_mul_of_infiniteNeg_not_infinitesimal_pos`, `infiniteNeg_mul_of_infinitePos_not_infinitesimal_neg`, `infiniteNeg_mul_of_not_infinitesimal_neg_infinitePos`, `infiniteNeg_mul_of_not_infinitesimal_pos_infiniteNeg`, `infiniteNeg_neg`, `infiniteNeg_of_tendsto_bot`, `infinitePos_abs_iff_infinite`, `infinitePos_abs_iff_infinite_abs`, `infinitePos_add_infinitePos`, `infinitePos_add_not_infinite`, `infinitePos_add_not_infiniteNeg`, `infinitePos_def`, `infinitePos_iff_infinite_and_pos`, `infinitePos_iff_infinite_of_nonneg`, `infinitePos_iff_infinite_of_pos`, `infinitePos_iff_infinitesimal_inv_pos`, `infinitePos_mul_infiniteNeg`, `infinitePos_mul_infinitePos`, `infinitePos_mul_of_infiniteNeg_not_infinitesimal_neg`, `infinitePos_mul_of_infinitePos_not_infinitesimal_pos`, `infinitePos_mul_of_not_infinitesimal_neg_infiniteNeg`, `infinitePos_mul_of_not_infinitesimal_pos_infinitePos`, `infinitePos_neg`, `infinitePos_of_tendsto_top`, `infinitePos_omega`, `infinite_abs_iff`, `infinite_iff_abs_lt_abs`, `infinite_iff_infinitesimal_inv`, `infinite_iff_not_exists_st`, `infinite_mul_of_infinite_not_infinitesimal`, `infinite_mul_of_not_infinitesimal_infinite`, `infinite_neg`, `infinite_of_infinitesimal_inv`, `infinite_omega`, `infinitesimal_def`, `infinitesimal_epsilon`, `infinitesimal_iff_infinite_inv`, `infinitesimal_inv_of_infinite`, `infinitesimal_neg`, `infinitesimal_neg_iff_infiniteNeg_inv`, `infinitesimal_of_tendsto_zero`, `infinitesimal_pos_iff_infinitePos_inv`, `infinitesimal_real_iff`, `infinitesimal_sub_st`, `infinitesimal_zero`, `instIsStrictOrderedRing`, `inv_epsilon`, `inv_omega`, `isSt_iff_abs_sub_lt_delta`, `isSt_iff_tendsto`, `isSt_inj_real`, `isSt_ofSeq_iff_tendsto`, `isSt_of_tendsto`, `isSt_real_iff_eq`, `isSt_refl_real`, `isSt_sSup`, `isSt_st`, `isSt_st'`, `isSt_st_of_exists_st`, `isSt_symm_real`, `isSt_trans_real`, `lt_neg_of_pos_of_infinitesimal`, `lt_of_pos_of_infinitesimal`, `lt_of_st_lt`, `lt_of_tendsto_atBot`, `lt_of_tendsto_atTop`, `lt_of_tendsto_zero_of_pos`, `neg_lt_of_tendsto_zero_of_pos`, `not_infiniteNeg_add_infinitePos`, `not_infinitePos_add_infiniteNeg`, `not_infinite_add`, `not_infinite_iff_exist_lt_gt`, `not_infinite_mul`, `not_infinite_neg`, `not_infinite_of_exists_st`, `not_infinite_real`, `not_infinite_zero`, `not_real_of_infinitesimal_ne_zero`, `ofSeq_le_ofSeq`, `ofSeq_lt_ofSeq`, `ofSeq_surjective`, `omega_ne_zero`, `omega_pos`, `st_add`, `st_eq_sSup`, `st_id_real`, `st_inv`, `st_le_of_le`, `st_mul`, `st_neg`, `stdPart_coe`, `stdPart_epsilon`, `stdPart_of_tendsto`, `stdPart_omega`, `tendsto_atBot_iff`, `tendsto_atTop_iff`, `tendsto_iff_forall`, `tendsto_ofSeq`	184
Total	200

Hyperreal

Definitions

Name	Category	Theorems
`InfiniteNeg` 📖	MathDef	12 math math: `infiniteNeg_of_tendsto_bot`, `InfinitePos.neg`, `infinitePos_neg`, `infiniteNeg_iff_infinite_and_neg`, `InfinitePos.not_infiniteNeg`, `infinitesimal_neg_iff_infiniteNeg_inv`, `infiniteNeg_def`, `infiniteNeg_iff_infinite_of_neg`, `infiniteNeg_iff_infinitesimal_inv_neg`, `infiniteNeg_neg`, `infiniteNeg_mul_of_not_infinitesimal_neg_infinitePos`, `infiniteNeg_mul_of_infinitePos_not_infinitesimal_neg`
`InfinitePos` 📖	MathDef	17 math math: `InfiniteNeg.neg`, `infinitePos_of_tendsto_top`, `infinitePos_omega`, `infinitePos_mul_of_infiniteNeg_not_infinitesimal_neg`, `infinitePos_neg`, `infinitePos_iff_infinite_and_pos`, `infiniteNeg_mul_infiniteNeg`, `infinitePos_iff_infinitesimal_inv_pos`, `infinitePos_abs_iff_infinite_abs`, `infinitePos_iff_infinite_of_pos`, `infinitePos_iff_infinite_of_nonneg`, `infiniteNeg_neg`, `infinitePos_def`, `infinitesimal_pos_iff_infinitePos_inv`, `infinitePos_mul_of_not_infinitesimal_neg_infiniteNeg`, `infinitePos_abs_iff_infinite`, `InfiniteNeg.not_infinitePos`
`Infinitesimal` 📖	MathDef	19 math math: `InfiniteNeg.not_infinitesimal`, `infinitesimal_def`, `infinitesimal_inv_of_infinite`, `infinite_iff_infinitesimal_inv`, `InfinitePos.not_infinitesimal`, `infinitePos_iff_infinitesimal_inv_pos`, `infinitesimal_sub_st`, `infinitesimal_of_tendsto_zero`, `infinitesimal_neg_iff_infiniteNeg_inv`, `infinitesimal_iff_infinite_inv`, `infinitesimal_real_iff`, `infiniteNeg_iff_infinitesimal_inv_neg`, `infinitesimal_epsilon`, `infinitesimal_zero`, `infinitesimal_neg`, `abs_lt_real_iff_infinitesimal`, `infinitesimal_pos_iff_infinitePos_inv`, `Infinite.not_infinitesimal`, `IsSt.infinitesimal_sub`
`IsSt` 📖	MathDef	13 math math: `isSt_symm_real`, `isSt_iff_abs_sub_lt_delta`, `isSt_sSup`, `isSt_st`, `exists_st_iff_not_infinite`, `isSt_refl_real`, `infinite_iff_not_exists_st`, `isSt_of_tendsto`, `isSt_real_iff_eq`, `isSt_iff_tendsto`, `exists_st_of_not_infinite`, `isSt_st'`, `isSt_ofSeq_iff_tendsto`
`coeRingHom` 📖	CompOp	1 math math: `coeRingHom_toFun`
`epsilon` 📖	CompOp	10 math math: `epsilon_lt_of_pos`, `epsilon_mul_omega`, `inv_omega`, `epsilon_lt_pos`, `inv_epsilon`, `epsilon_lt_of_neg`, `infinitesimal_epsilon`, `stdPart_epsilon`, `epsilon_pos`, `archimedeanClassMk_epsilon_pos`
`instCoeTCReal` 📖	CompOp	—
`instField` 📖	CompOp	96 math math: `InfiniteNeg.neg`, `infinitePos_add_not_infiniteNeg`, `infinite_neg`, `not_infinite_zero`, `neg_lt_of_tendsto_zero_of_pos`, `not_infiniteNeg_add_infinitePos`, `epsilon_mul_omega`, `not_infinitePos_add_infiniteNeg`, `coe_ofNat`, `InfinitePos.neg`, `infinitesimal_def`, `Infinitesimal.add`, `InfiniteNeg.lt_zero`, `Infinite.mul`, `infinitePos_add_not_infinite`, `infinitesimal_inv_of_infinite`, `infinite_abs_iff`, `infinite_mul_of_not_infinitesimal_infinite`, `archimdeanClassMk_coe`, `inv_omega`, `infinite_iff_infinitesimal_inv`, `infinitePos_neg`, `isSt_iff_abs_sub_lt_delta`, `archimedeanClassMk_neg_of_tendsto_atBot`, `coe_eq_one`, `st_mul`, `stdPart_coe`, `infinitePos_iff_infinite_and_pos`, `coe_nonneg`, `infiniteNeg_mul_infiniteNeg`, `infinitePos_iff_infinitesimal_inv_pos`, `coe_pos`, `archimedeanClassMk_neg_of_tendsto_atTop`, `IsSt.add`, `infiniteNeg_iff_infinite_and_neg`, `archimedeanClassMk_pos_of_tendsto`, `infinitesimal_sub_st`, `infinitePos_abs_iff_infinite_abs`, `inv_epsilon`, `archimedeanClassMk_nonneg_of_tendsto`, `IsSt.mul`, `IsSt.inv`, `infinitePos_mul_infiniteNeg`, `coe_inv`, `infinitesimal_neg_iff_infiniteNeg_inv`, `infiniteNeg_mul_infinitePos`, `IsSt.sub`, `Infinitesimal.mul`, `instIsStrictOrderedRing`, `coe_eq_zero`, `coe_zero`, `lt_neg_of_pos_of_infinitesimal`, `infinitesimal_iff_infinite_inv`, `not_infinite_neg`, `infiniteNeg_add_infiniteNeg`, `not_infinite_add`, `coe_one`, `infinite_mul_of_infinite_not_infinitesimal`, `infinite_iff_abs_lt_abs`, `omega_pos`, `coe_add`, `infiniteNeg_iff_infinitesimal_inv_neg`, `archimedeanClassMk_omega_neg`, `archimedeanClassMk_coe_nonneg`, `tendsto_atBot_iff`, `not_infinite_mul`, `stdPart_of_tendsto`, `infinitesimal_zero`, `coe_div`, `infiniteNeg_neg`, `coe_abs`, `st_inv`, `abs_omega`, `InfinitePos.pos`, `infinitesimal_neg`, `coe_neg`, `stdPart_omega`, `abs_lt_real_iff_infinitesimal`, `infinitesimal_pos_iff_infinitePos_inv`, `coe_mul`, `infiniteNeg_add_not_infinitePos`, `infinitePos_add_infinitePos`, `infinitePos_abs_iff_infinite`, `IsSt.neg`, `infinitePos_mul_infinitePos`, `stdPart_epsilon`, `st_neg`, `st_add`, `coe_sub`, `infiniteNeg_add_not_infinite`, `epsilon_pos`, `archimedeanClassMk_epsilon_pos`, `IsSt.infinitesimal_sub`, `tendsto_atTop_iff`, `Infinitesimal.neg`, `coeRingHom_toFun`
`instLinearOrder` 📖	CompOp	63 math math: `epsilon_lt_of_pos`, `neg_lt_of_tendsto_zero_of_pos`, `infinitesimal_def`, `coe_lt_omega`, `InfiniteNeg.lt_zero`, `infinite_abs_iff`, `not_infinite_iff_exist_lt_gt`, `archimdeanClassMk_coe`, `tendsto_iff_forall`, `isSt_iff_abs_sub_lt_delta`, `archimedeanClassMk_neg_of_tendsto_atBot`, `isSt_sSup`, `stdPart_coe`, `infinitePos_iff_infinite_and_pos`, `epsilon_lt_pos`, `coe_nonneg`, `infinitePos_iff_infinitesimal_inv_pos`, `coe_pos`, `archimedeanClassMk_neg_of_tendsto_atTop`, `infiniteNeg_iff_infinite_and_neg`, `lt_of_tendsto_atTop`, `archimedeanClassMk_pos_of_tendsto`, `infinitePos_abs_iff_infinite_abs`, `archimedeanClassMk_nonneg_of_tendsto`, `epsilon_lt_of_neg`, `infinitesimal_neg_iff_infiniteNeg_inv`, `infiniteNeg_def`, `instIsStrictOrderedRing`, `coe_min`, `lt_neg_of_pos_of_infinitesimal`, `lt_of_pos_of_infinitesimal`, `lt_of_tendsto_atBot`, `infinite_iff_abs_lt_abs`, `ofSeq_le_ofSeq`, `omega_pos`, `infiniteNeg_iff_infinitesimal_inv_neg`, `archimedeanClassMk_omega_neg`, `archimedeanClassMk_coe_nonneg`, `tendsto_atBot_iff`, `lt_of_tendsto_zero_of_pos`, `coe_max`, `stdPart_of_tendsto`, `lt_of_st_lt`, `coe_abs`, `IsSt.lt`, `abs_omega`, `InfinitePos.pos`, `infinitePos_def`, `stdPart_omega`, `abs_lt_real_iff_infinitesimal`, `infinitesimal_pos_iff_infinitePos_inv`, `coe_le_coe`, `coe_lt_coe`, `st_eq_sSup`, `infinitePos_abs_iff_infinite`, `stdPart_epsilon`, `ofSeq_lt_ofSeq`, `gt_of_neg_of_infinitesimal`, `gt_of_tendsto_zero_of_neg`, `epsilon_pos`, `archimedeanClassMk_epsilon_pos`, `tendsto_atTop_iff`, `coeRingHom_toFun`
`ofReal` 📖	CompOp	53 math math: `epsilon_lt_of_pos`, `neg_lt_of_tendsto_zero_of_pos`, `coe_eq_coe`, `coe_ofNat`, `infinitesimal_def`, `coe_lt_omega`, `isSt_symm_real`, `not_infinite_iff_exist_lt_gt`, `archimdeanClassMk_coe`, `tendsto_iff_forall`, `isSt_iff_abs_sub_lt_delta`, `isSt_sSup`, `coe_eq_one`, `stdPart_coe`, `epsilon_lt_pos`, `coe_nonneg`, `coe_pos`, `lt_of_tendsto_atTop`, `infinitesimal_sub_st`, `epsilon_lt_of_neg`, `isSt_refl_real`, `coe_inv`, `st_id_real`, `infiniteNeg_def`, `coe_eq_zero`, `coe_zero`, `coe_min`, `lt_neg_of_pos_of_infinitesimal`, `lt_of_pos_of_infinitesimal`, `coe_one`, `infinitesimal_real_iff`, `lt_of_tendsto_atBot`, `infinite_iff_abs_lt_abs`, `coe_add`, `archimedeanClassMk_coe_nonneg`, `lt_of_tendsto_zero_of_pos`, `coe_max`, `coe_div`, `isSt_real_iff_eq`, `coe_abs`, `not_infinite_real`, `infinitePos_def`, `coe_neg`, `abs_lt_real_iff_infinitesimal`, `coe_mul`, `coe_le_coe`, `coe_lt_coe`, `st_eq_sSup`, `gt_of_neg_of_infinitesimal`, `coe_sub`, `gt_of_tendsto_zero_of_neg`, `IsSt.infinitesimal_sub`, `coeRingHom_toFun`
`ofSeq` 📖	CompOp	12 math math: `infiniteNeg_of_tendsto_bot`, `infinitePos_of_tendsto_top`, `neg_lt_of_tendsto_zero_of_pos`, `infinitesimal_of_tendsto_zero`, `ofSeq_surjective`, `ofSeq_le_ofSeq`, `isSt_of_tendsto`, `lt_of_tendsto_zero_of_pos`, `tendsto_ofSeq`, `ofSeq_lt_ofSeq`, `isSt_ofSeq_iff_tendsto`, `gt_of_tendsto_zero_of_neg`
`omega` 📖	CompOp	10 math math: `infinitePos_omega`, `epsilon_mul_omega`, `coe_lt_omega`, `inv_omega`, `inv_epsilon`, `infinite_omega`, `omega_pos`, `archimedeanClassMk_omega_neg`, `abs_omega`, `stdPart_omega`
`st` 📖	CompOp	14 math math: `IsSt.st_eq`, `isSt_st`, `st_mul`, `Infinite.st_eq`, `infinitesimal_sub_st`, `st_id_real`, `IsSt.isSt_st`, `st_le_of_le`, `isSt_st_of_exists_st`, `st_inv`, `isSt_st'`, `st_eq_sSup`, `st_neg`, `st_add`
`termε` 📖	CompOp	—
`termω` 📖	CompOp	—
`«termℝ*»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`abs_lt_real_iff_infinitesimal` 📖	mathematical	—	`Infinitesimal` `Hyperreal` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrder` `abs` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `instField` `ofReal`	—	`abs_lt` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `instIsStrictOrderedRing` `covariant_swap_add_of_covariant_add` `infinitesimal_def` `abs_pos` `Real.instIsOrderedAddMonoid` `coe_abs` `abs_of_pos` `coe_pos` `LT.lt.ne'`
`abs_omega` 📖	mathematical	—	`abs` `Hyperreal` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrder` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `instField` `omega`	—	`abs_of_pos` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `instIsStrictOrderedRing` `omega_pos`
`archimdeanClassMk_coe` 📖	mathematical	—	`Hyperreal` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `instField` `instLinearOrder` `IsOrderedRing.toIsOrderedAddMonoid` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `IsStrictOrderedRing.toIsOrderedRing` `instIsStrictOrderedRing` `ofReal` `ArchimedeanClass` `ArchimedeanClass.instZero` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	—	`ArchimedeanClass.mk_map_of_archimedean'` `instIsStrictOrderedRing` `Real.instIsStrictOrderedRing` `Real.instArchimedean`
`archimedeanClassMk_coe_nonneg` 📖	mathematical	—	`ArchimedeanClass` `Hyperreal` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `instField` `instLinearOrder` `IsOrderedRing.toIsOrderedAddMonoid` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `IsStrictOrderedRing.toIsOrderedRing` `instIsStrictOrderedRing` `Preorder.toLE` `PartialOrder.toPreorder` `ArchimedeanClass.instLinearOrder` `ArchimedeanClass.instZero` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `ofReal`	—	`ArchimedeanClass.mk_map_nonneg_of_archimedean` `instIsStrictOrderedRing` `Real.instIsStrictOrderedRing` `Real.instArchimedean`
`archimedeanClassMk_epsilon_pos` 📖	mathematical	—	`ArchimedeanClass` `Hyperreal` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `instField` `instLinearOrder` `IsOrderedRing.toIsOrderedAddMonoid` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `IsStrictOrderedRing.toIsOrderedRing` `instIsStrictOrderedRing` `Preorder.toLT` `PartialOrder.toPreorder` `ArchimedeanClass.instLinearOrder` `ArchimedeanClass.instZero` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `epsilon`	—	`IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `instIsStrictOrderedRing` `archimedeanClassMk_omega_neg`
`archimedeanClassMk_neg_of_tendsto_atBot` 📖	mathematical	`Filter.Germ.Tendsto` `Real` `Ultrafilter.toFilter` `Filter.hyperfilter` `instInfiniteNat` `Filter.atBot` `Real.instPreorder`	`ArchimedeanClass` `Hyperreal` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `instField` `instLinearOrder` `IsOrderedRing.toIsOrderedAddMonoid` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `IsStrictOrderedRing.toIsOrderedRing` `instIsStrictOrderedRing` `Preorder.toLT` `PartialOrder.toPreorder` `ArchimedeanClass.instLinearOrder` `ArchimedeanClass.instZero` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	—	`instInfiniteNat` `lt_of_tendsto_atBot` `abs_one` `IsStrictOrderedRing.toIsOrderedRing` `instIsStrictOrderedRing` `nsmul_eq_mul` `mul_one` `abs_of_neg` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add`
`archimedeanClassMk_neg_of_tendsto_atTop` 📖	mathematical	`Filter.Germ.Tendsto` `Real` `Ultrafilter.toFilter` `Filter.hyperfilter` `instInfiniteNat` `Filter.atTop` `Real.instPreorder`	`ArchimedeanClass` `Hyperreal` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `instField` `instLinearOrder` `IsOrderedRing.toIsOrderedAddMonoid` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `IsStrictOrderedRing.toIsOrderedRing` `instIsStrictOrderedRing` `Preorder.toLT` `PartialOrder.toPreorder` `ArchimedeanClass.instLinearOrder` `ArchimedeanClass.instZero` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	—	`instInfiniteNat` `lt_of_tendsto_atTop` `abs_one` `IsStrictOrderedRing.toIsOrderedRing` `instIsStrictOrderedRing` `nsmul_eq_mul` `mul_one` `abs_of_pos` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid`
`archimedeanClassMk_nonneg_of_tendsto` 📖	mathematical	`Filter.Germ.Tendsto` `Real` `Ultrafilter.toFilter` `Filter.hyperfilter` `instInfiniteNat` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace`	`ArchimedeanClass` `Hyperreal` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `instField` `instLinearOrder` `IsOrderedRing.toIsOrderedAddMonoid` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `IsStrictOrderedRing.toIsOrderedRing` `instIsStrictOrderedRing` `Preorder.toLE` `PartialOrder.toPreorder` `ArchimedeanClass.instLinearOrder` `ArchimedeanClass.instZero` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	—	`instInfiniteNat` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `instIsStrictOrderedRing` `NoMinOrder.exists_lt` `instNoMinOrderOfNontrivial` `Real.instIsOrderedRing` `Real.instNontrivial` `NoMaxOrder.exists_gt` `instNoMaxOrderOfNontrivial` `ArchimedeanClass.mk_nonneg_of_le_of_le_of_archimedean` `Real.instIsStrictOrderedRing` `Real.instArchimedean` `tendsto_iff_forall`
`archimedeanClassMk_omega_neg` 📖	mathematical	—	`ArchimedeanClass` `Hyperreal` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `instField` `instLinearOrder` `IsOrderedRing.toIsOrderedAddMonoid` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `IsStrictOrderedRing.toIsOrderedRing` `instIsStrictOrderedRing` `Preorder.toLT` `PartialOrder.toPreorder` `ArchimedeanClass.instLinearOrder` `omega` `ArchimedeanClass.instZero` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	—	`abs_one` `IsStrictOrderedRing.toIsOrderedRing` `instIsStrictOrderedRing` `nsmul_eq_mul` `mul_one` `abs_omega` `coe_lt_omega`
`archimedeanClassMk_pos_of_tendsto` 📖	mathematical	`Filter.Germ.Tendsto` `Real` `Ultrafilter.toFilter` `Filter.hyperfilter` `instInfiniteNat` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instZero`	`ArchimedeanClass` `Hyperreal` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `instField` `instLinearOrder` `IsOrderedRing.toIsOrderedAddMonoid` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `IsStrictOrderedRing.toIsOrderedRing` `instIsStrictOrderedRing` `Preorder.toLT` `PartialOrder.toPreorder` `ArchimedeanClass.instLinearOrder` `ArchimedeanClass.instZero` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	—	`instInfiniteNat` `LE.le.lt_of_ne'` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `instIsStrictOrderedRing` `archimedeanClassMk_nonneg_of_tendsto` `IsOrderedRing.toIsStrictOrderedRing` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `ArchimedeanClass.stdPart_eq_zero` `stdPart_of_tendsto`
`coeRingHom_toFun` 📖	mathematical	—	`DFunLike.coe` `OrderRingHom` `Real` `Hyperreal` `Semiring.toNonAssocSemiring` `Real.semiring` `Real.instPreorder` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `instField` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrder` `OrderRingHom.instFunLike` `coeRingHom` `ofReal`	—	`instInfiniteNat`
`coe_abs` 📖	mathematical	—	`ofReal` `abs` `Real` `Real.lattice` `Real.instAddGroup` `Hyperreal` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrder` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `instField`	—	`Filter.Germ.const_abs` `instInfiniteNat`
`coe_add` 📖	mathematical	—	`ofReal` `Real` `Real.instAdd` `Hyperreal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instField`	—	—
`coe_div` 📖	mathematical	—	`ofReal` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Hyperreal` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing` `instField`	—	—
`coe_eq_coe` 📖	mathematical	—	`ofReal`	—	`instInfiniteNat` `Ultrafilter.neBot`
`coe_eq_one` 📖	mathematical	—	`ofReal` `Hyperreal` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `instField` `Real` `Real.instOne`	—	`coe_eq_coe`
`coe_eq_zero` 📖	mathematical	—	`ofReal` `Hyperreal` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instField` `Real` `Real.instZero`	—	`coe_eq_coe`
`coe_inv` 📖	mathematical	—	`ofReal` `Real` `Real.instInv` `Hyperreal` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `Field.toSemifield` `instField`	—	—
`coe_le_coe` 📖	mathematical	—	`Hyperreal` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrder` `ofReal` `Real` `Real.instLE`	—	`Filter.Germ.const_le_iff` `instInfiniteNat` `Ultrafilter.neBot`
`coe_lt_coe` 📖	mathematical	—	`Hyperreal` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrder` `ofReal` `Real` `Real.instLT`	—	`Filter.Germ.const_lt_iff` `instInfiniteNat`
`coe_lt_omega` 📖	mathematical	—	`Hyperreal` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrder` `ofReal` `omega`	—	`instInfiniteNat` `ofSeq_lt_ofSeq` `Filter.Eventually.filter_mono` `Nat.hyperfilter_le_atTop` `exists_nat_gt` `Real.instIsStrictOrderedRing` `Real.instArchimedean` `Filter.eventually_atTop` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `LT.lt.trans_le` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `IsStrictOrderedRing.toCharZero`
`coe_max` 📖	mathematical	—	`ofReal` `Real` `Real.instMax` `Hyperreal` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrder`	—	`Filter.Germ.const_max` `instInfiniteNat`
`coe_min` 📖	mathematical	—	`ofReal` `Real` `Real.instMin` `Hyperreal` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrder`	—	`Filter.Germ.const_min` `instInfiniteNat`
`coe_mul` 📖	mathematical	—	`ofReal` `Real` `Real.instMul` `Hyperreal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instField`	—	—
`coe_ne_coe` 📖	—	—	—	—	`Iff.not` `coe_eq_coe`
`coe_ne_one` 📖	—	—	—	—	`coe_ne_coe`
`coe_ne_zero` 📖	—	—	—	—	`coe_ne_coe`
`coe_neg` 📖	mathematical	—	`ofReal` `Real` `Real.instNeg` `Hyperreal` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `instField`	—	—
`coe_nonneg` 📖	mathematical	—	`Hyperreal` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instField` `ofReal` `Real` `Real.instLE` `Real.instZero`	—	`coe_le_coe`
`coe_ofNat` 📖	mathematical	—	`ofReal` `Hyperreal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `instField`	—	—
`coe_one` 📖	mathematical	—	`ofReal` `Real` `Real.instOne` `Hyperreal` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `instField`	—	—
`coe_pos` 📖	mathematical	—	`Hyperreal` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instField` `ofReal` `Real` `Real.instLT` `Real.instZero`	—	`coe_lt_coe`
`coe_sub` 📖	mathematical	—	`ofReal` `Real` `Real.instSub` `Hyperreal` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `instField`	—	—
`coe_zero` 📖	mathematical	—	`ofReal` `Real` `Real.instZero` `Hyperreal` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instField`	—	—
`epsilon_lt_of_neg` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`Hyperreal` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrder` `ofReal` `epsilon`	—	`ArchimedeanClass.lt_of_neg_of_archimedean` `instIsStrictOrderedRing` `Real.instIsStrictOrderedRing` `Real.instArchimedean` `archimedeanClassMk_epsilon_pos`
`epsilon_lt_of_pos` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`Hyperreal` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrder` `epsilon` `ofReal`	—	`ArchimedeanClass.lt_of_pos_of_archimedean` `instIsStrictOrderedRing` `Real.instIsStrictOrderedRing` `Real.instArchimedean` `archimedeanClassMk_epsilon_pos`
`epsilon_lt_pos` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`Hyperreal` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrder` `epsilon` `ofReal`	—	`epsilon_lt_of_pos`
`epsilon_mul_omega` 📖	mathematical	—	`Hyperreal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instField` `epsilon` `omega` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing`	—	`inv_mul_cancel₀` `omega_ne_zero`
`epsilon_ne_zero` 📖	—	—	—	—	`LT.lt.ne'` `epsilon_pos`
`epsilon_pos` 📖	mathematical	—	`Hyperreal` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instField` `epsilon`	—	`inv_pos_of_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `instIsStrictOrderedRing` `omega_pos`
`eq_of_isSt_real` 📖	—	`IsSt` `ofReal`	—	—	`IsSt.unique` `isSt_refl_real`
`exists_st_iff_not_infinite` 📖	mathematical	—	`IsSt` `Infinite`	—	`not_infinite_of_exists_st` `exists_st_of_not_infinite`
`exists_st_of_not_infinite` 📖	mathematical	`Infinite`	`IsSt`	—	`isSt_sSup`
`gt_of_neg_of_infinitesimal` 📖	mathematical	`Infinitesimal` `Real` `Real.instLT` `Real.instZero`	`Hyperreal` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrder` `ofReal`	—	`infinitesimal_def` `neg_pos` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `neg_neg`
`gt_of_tendsto_zero_of_neg` 📖	mathematical	`Filter.Tendsto` `Real` `Filter.atTop` `Nat.instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instZero` `Real.instLT`	`Hyperreal` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrder` `ofReal` `ofSeq`	—	`neg_neg` `coe_neg` `neg_lt_of_tendsto_zero_of_pos` `neg_pos` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid`
`infiniteNeg_add_infiniteNeg` 📖	mathematical	`InfiniteNeg`	`Hyperreal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instField`	—	`infiniteNeg_add_not_infinitePos` `InfiniteNeg.not_infinitePos`
`infiniteNeg_add_not_infinite` 📖	mathematical	`InfiniteNeg` `Infinite`	`Hyperreal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instField`	—	`infiniteNeg_add_not_infinitePos`
`infiniteNeg_add_not_infinitePos` 📖	mathematical	`InfiniteNeg` `InfinitePos`	`Hyperreal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instField`	—	`infinitePos_neg` `infiniteNeg_neg` `neg_add` `infinitePos_add_not_infiniteNeg`
`infiniteNeg_def` 📖	mathematical	—	`InfiniteNeg` `Hyperreal` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrder` `ofReal`	—	—
`infiniteNeg_iff_infinite_and_neg` 📖	mathematical	—	`InfiniteNeg` `Infinite` `Hyperreal` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instField`	—	`not_lt_of_gt`
`infiniteNeg_iff_infinite_of_neg` 📖	mathematical	`Hyperreal` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instField`	`InfiniteNeg` `Infinite`	—	`LT.lt.not_gt` `InfinitePos.pos`
`infiniteNeg_iff_infinitesimal_inv_neg` 📖	mathematical	—	`InfiniteNeg` `Infinitesimal` `Hyperreal` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `Field.toSemifield` `instField` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	—	`infinitePos_neg` `infinitePos_iff_infinitesimal_inv_pos` `inv_neg` `neg_pos` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `instIsStrictOrderedRing` `infinitesimal_neg`
`infiniteNeg_mul_infiniteNeg` 📖	mathematical	`InfiniteNeg`	`InfinitePos` `Hyperreal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instField`	—	`infinitePos_mul_of_infiniteNeg_not_infinitesimal_neg` `InfiniteNeg.not_infinitesimal`
`infiniteNeg_mul_infinitePos` 📖	mathematical	`InfiniteNeg` `InfinitePos`	`Hyperreal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instField`	—	`infiniteNeg_mul_of_infiniteNeg_not_infinitesimal_pos` `InfinitePos.not_infinitesimal`
`infiniteNeg_mul_of_infiniteNeg_not_infinitesimal_pos` 📖	mathematical	`InfiniteNeg` `Infinitesimal` `Hyperreal` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instField`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`infinitePos_neg` `neg_mul_eq_neg_mul` `infinitePos_mul_of_infinitePos_not_infinitesimal_pos`
`infiniteNeg_mul_of_infinitePos_not_infinitesimal_neg` 📖	mathematical	`InfinitePos` `Infinitesimal` `Hyperreal` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instField`	`InfiniteNeg` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`infinitePos_neg` `neg_pos` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `instIsStrictOrderedRing` `neg_mul_eq_mul_neg` `infinitesimal_neg` `infinitePos_mul_of_infinitePos_not_infinitesimal_pos`
`infiniteNeg_mul_of_not_infinitesimal_neg_infinitePos` 📖	mathematical	`Infinitesimal` `Hyperreal` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instField` `InfinitePos`	`InfiniteNeg` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`infiniteNeg_mul_of_infinitePos_not_infinitesimal_neg` `mul_comm`
`infiniteNeg_mul_of_not_infinitesimal_pos_infiniteNeg` 📖	mathematical	`Infinitesimal` `Hyperreal` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instField` `InfiniteNeg`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`mul_comm` `infiniteNeg_mul_of_infiniteNeg_not_infinitesimal_pos`
`infiniteNeg_neg` 📖	mathematical	—	`InfiniteNeg` `Hyperreal` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `instField` `InfinitePos`	—	`InfiniteNeg.neg` `neg_neg` `InfinitePos.neg`
`infiniteNeg_of_tendsto_bot` 📖	mathematical	`Filter.Tendsto` `Real` `Filter.atTop` `Nat.instPreorder` `Filter.atBot` `Real.instPreorder`	`InfiniteNeg` `ofSeq`	—	`Filter.tendsto_atTop_atBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `lt_imp_lt_of_le_imp_le` `le_of_lt` `lt_of_lt_of_le` `sub_one_lt` `Real.instZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `instInfiniteNat` `Filter.Germ.coe_lt` `Filter.mem_hyperfilter_of_finite_compl` `Set.Finite.subset` `Set.finite_le_nat`
`infinitePos_abs_iff_infinite` 📖	mathematical	—	`InfinitePos` `abs` `Hyperreal` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrder` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `instField` `Infinite`	—	`infinitePos_abs_iff_infinite_abs` `infinite_abs_iff`
`infinitePos_abs_iff_infinite_abs` 📖	mathematical	—	`InfinitePos` `abs` `Hyperreal` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrder` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `instField` `Infinite`	—	`infinitePos_iff_infinite_of_nonneg` `abs_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `instIsStrictOrderedRing` `covariant_swap_add_of_covariant_add`
`infinitePos_add_infinitePos` 📖	mathematical	`InfinitePos`	`Hyperreal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instField`	—	`infinitePos_add_not_infiniteNeg` `InfinitePos.not_infiniteNeg`
`infinitePos_add_not_infinite` 📖	mathematical	`InfinitePos` `Infinite`	`Hyperreal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instField`	—	`infinitePos_add_not_infiniteNeg`
`infinitePos_add_not_infiniteNeg` 📖	mathematical	`InfinitePos` `InfiniteNeg`	`Hyperreal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instField`	—	`neg_add_cancel_right` `add_lt_add_of_lt_of_le` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `instIsStrictOrderedRing` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `not_lt`
`infinitePos_def` 📖	mathematical	—	`InfinitePos` `Hyperreal` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrder` `ofReal`	—	—
`infinitePos_iff_infinite_and_pos` 📖	mathematical	—	`InfinitePos` `Infinite` `Hyperreal` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instField`	—	`not_lt_of_gt`
`infinitePos_iff_infinite_of_nonneg` 📖	mathematical	`Hyperreal` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instField`	`InfinitePos` `Infinite`	—	`LT.lt.not_ge` `InfiniteNeg.lt_zero`
`infinitePos_iff_infinite_of_pos` 📖	mathematical	`Hyperreal` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instField`	`InfinitePos` `Infinite`	—	`infinitePos_iff_infinite_of_nonneg` `LT.lt.le`
`infinitePos_iff_infinitesimal_inv_pos` 📖	mathematical	—	`InfinitePos` `Infinitesimal` `Hyperreal` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `Field.toSemifield` `instField` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	—	`infinitesimal_def` `lt_trans` `coe_lt_coe` `neg_neg_of_pos` `Real.instIsOrderedAddMonoid` `inv_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `instIsStrictOrderedRing` `inv_lt_of_inv_lt₀` `instInfiniteNat` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `by_cases` `lt_of_le_of_lt` `coe_le_coe` `le_abs_self` `inv_lt_inv₀` `abs_pos` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsStrictOrderedRing`
`infinitePos_mul_infiniteNeg` 📖	mathematical	`InfinitePos` `InfiniteNeg`	`Hyperreal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instField`	—	`infiniteNeg_mul_of_infinitePos_not_infinitesimal_neg` `InfiniteNeg.not_infinitesimal`
`infinitePos_mul_infinitePos` 📖	mathematical	`InfinitePos`	`Hyperreal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instField`	—	`infinitePos_mul_of_infinitePos_not_infinitesimal_pos` `InfinitePos.not_infinitesimal`
`infinitePos_mul_of_infiniteNeg_not_infinitesimal_neg` 📖	mathematical	`InfiniteNeg` `Infinitesimal` `Hyperreal` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instField`	`InfinitePos` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`infinitePos_neg` `neg_pos` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `instIsStrictOrderedRing` `neg_mul_neg` `infinitesimal_neg` `infinitePos_mul_of_infinitePos_not_infinitesimal_pos`
`infinitePos_mul_of_infinitePos_not_infinitesimal_pos` 📖	mathematical	`InfinitePos` `Infinitesimal` `Hyperreal` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instField`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`infinitesimal_def` `abs_of_pos` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `instIsStrictOrderedRing` `not_lt` `abs_lt` `covariant_swap_add_of_covariant_add` `div_mul_cancel₀` `ne_of_gt` `coe_mul` `mul_lt_mul` `IsOrderedRing.toPosMulMono` `IsStrictOrderedRing.toMulPosStrictMono` `coe_lt_coe` `le_of_lt`
`infinitePos_mul_of_not_infinitesimal_neg_infiniteNeg` 📖	mathematical	`Infinitesimal` `Hyperreal` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instField` `InfiniteNeg`	`InfinitePos` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`infinitePos_mul_of_infiniteNeg_not_infinitesimal_neg` `mul_comm`
`infinitePos_mul_of_not_infinitesimal_pos_infinitePos` 📖	mathematical	`Infinitesimal` `Hyperreal` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instField` `InfinitePos`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`infinitePos_mul_of_infinitePos_not_infinitesimal_pos` `mul_comm`
`infinitePos_neg` 📖	mathematical	—	`InfinitePos` `Hyperreal` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `instField` `InfiniteNeg`	—	`InfinitePos.neg` `neg_neg` `InfiniteNeg.neg`
`infinitePos_of_tendsto_top` 📖	mathematical	`Filter.Tendsto` `Real` `Filter.atTop` `Nat.instPreorder` `Real.instPreorder`	`InfinitePos` `ofSeq`	—	`Filter.tendsto_atTop_atTop` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `lt_imp_lt_of_le_imp_le` `le_of_lt` `lt_of_le_of_lt` `lt_add_one` `Real.instZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `instInfiniteNat` `Filter.Germ.coe_lt` `Filter.mem_hyperfilter_of_finite_compl` `Set.Finite.subset` `Set.finite_le_nat`
`infinitePos_omega` 📖	mathematical	—	`InfinitePos` `omega`	—	`infinitePos_iff_infinitesimal_inv_pos` `infinitesimal_epsilon` `epsilon_pos`
`infinite_abs_iff` 📖	mathematical	—	`Infinite` `abs` `Hyperreal` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrder` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `instField`	—	`le_total` `abs_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `instIsStrictOrderedRing` `abs_of_nonpos`
`infinite_iff_abs_lt_abs` 📖	mathematical	—	`Infinite` `Hyperreal` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrder` `abs` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `instField` `ofReal`	—	`infinitePos_abs_iff_infinite` `coe_abs` `LE.le.trans_lt` `le_abs_self`
`infinite_iff_infinitesimal_inv` 📖	mathematical	—	`Infinite` `Infinitesimal` `Hyperreal` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `Field.toSemifield` `instField`	—	`infinitesimal_inv_of_infinite` `infinite_of_infinitesimal_inv`
`infinite_iff_not_exists_st` 📖	mathematical	—	`Infinite` `IsSt`	—	`iff_not_comm` `exists_st_iff_not_infinite`
`infinite_mul_of_infinite_not_infinitesimal` 📖	mathematical	`Infinite` `Infinitesimal`	`Hyperreal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instField`	—	`lt_or_gt_of_ne` `isSt_refl_real` `infiniteNeg_mul_of_infinitePos_not_infinitesimal_neg` `infinitePos_mul_of_infinitePos_not_infinitesimal_pos` `infinitePos_mul_of_infiniteNeg_not_infinitesimal_neg` `infiniteNeg_mul_of_infiniteNeg_not_infinitesimal_pos`
`infinite_mul_of_not_infinitesimal_infinite` 📖	mathematical	`Infinitesimal` `Infinite`	`Hyperreal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instField`	—	`mul_comm` `infinite_mul_of_infinite_not_infinitesimal`
`infinite_neg` 📖	mathematical	—	`Infinite` `Hyperreal` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `instField`	—	`Iff.or` `infiniteNeg_neg` `infinitePos_neg`
`infinite_of_infinitesimal_inv` 📖	mathematical	`Infinitesimal` `Hyperreal` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `Field.toSemifield` `instField`	`Infinite`	—	`lt_or_gt_of_ne` `infiniteNeg_iff_infinitesimal_inv_neg` `instInfiniteNat` `inv_lt_zero` `IsOrderedRing.toPosMulMono` `IsStrictOrderedRing.toIsOrderedRing` `instIsStrictOrderedRing` `infinitePos_iff_infinitesimal_inv_pos` `inv_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono`
`infinite_omega` 📖	mathematical	—	`Infinite` `omega`	—	`infinite_iff_infinitesimal_inv` `omega_ne_zero` `infinitesimal_epsilon`
`infinitesimal_def` 📖	mathematical	—	`Infinitesimal` `Hyperreal` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrder` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `instField` `ofReal`	—	`zero_sub` `zero_add`
`infinitesimal_epsilon` 📖	mathematical	—	`Infinitesimal` `epsilon`	—	`infinitesimal_of_tendsto_zero` `tendsto_inv_atTop_nhds_zero_nat` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `NNRat.instContinuousSMulOfIsScalarTowerOfRat` `IsScalarTower.nnrat` `Rat.instCharZero` `NNRat.instContinuousSMulRatReal`
`infinitesimal_iff_infinite_inv` 📖	mathematical	—	`Infinitesimal` `Infinite` `Hyperreal` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `Field.toSemifield` `instField`	—	`inv_inv` `infinite_iff_infinitesimal_inv` `inv_ne_zero`
`infinitesimal_inv_of_infinite` 📖	mathematical	`Infinite`	`Infinitesimal` `Hyperreal` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `Field.toSemifield` `instField`	—	`infinitePos_iff_infinitesimal_inv_pos` `infiniteNeg_iff_infinitesimal_inv_neg`
`infinitesimal_neg` 📖	mathematical	—	`Infinitesimal` `Hyperreal` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `instField`	—	`Infinitesimal.neg` `neg_neg`
`infinitesimal_neg_iff_infiniteNeg_inv` 📖	mathematical	—	`InfiniteNeg` `Hyperreal` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `Field.toSemifield` `instField` `Infinitesimal` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	—	`infiniteNeg_iff_infinitesimal_inv_neg` `inv_inv`
`infinitesimal_of_tendsto_zero` 📖	mathematical	`Filter.Tendsto` `Real` `Filter.atTop` `Nat.instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instZero`	`Infinitesimal` `ofSeq`	—	`isSt_of_tendsto`
`infinitesimal_pos_iff_infinitePos_inv` 📖	mathematical	—	`InfinitePos` `Hyperreal` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `Field.toSemifield` `instField` `Infinitesimal` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	—	`infinitePos_iff_infinitesimal_inv_pos` `inv_inv`
`infinitesimal_real_iff` 📖	mathematical	—	`Infinitesimal` `ofReal` `Real` `Real.instZero`	—	`isSt_real_iff_eq`
`infinitesimal_sub_st` 📖	mathematical	`Infinite`	`Infinitesimal` `Hyperreal` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `instField` `ofReal` `st`	—	`IsSt.infinitesimal_sub` `isSt_st'`
`infinitesimal_zero` 📖	mathematical	—	`Infinitesimal` `Hyperreal` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instField`	—	`isSt_refl_real`
`instIsStrictOrderedRing` 📖	mathematical	—	`IsStrictOrderedRing` `Hyperreal` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `instField` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrder`	—	`instInfiniteNat` `Filter.Germ.instIsStrictOrderedRing` `Real.instIsStrictOrderedRing`
`inv_epsilon` 📖	mathematical	—	`Hyperreal` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `Field.toSemifield` `instField` `epsilon` `omega`	—	`inv_inv`
`inv_omega` 📖	mathematical	—	`Hyperreal` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `Field.toSemifield` `instField` `omega` `epsilon`	—	—
`isSt_iff_abs_sub_lt_delta` 📖	mathematical	—	`IsSt` `Hyperreal` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrder` `abs` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `instField` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `ofReal`	—	`IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `instIsStrictOrderedRing` `add_comm`
`isSt_iff_tendsto` 📖	mathematical	—	`IsSt` `Filter.Germ.Tendsto` `Real` `Ultrafilter.toFilter` `Filter.hyperfilter` `instInfiniteNat` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace`	—	`instInfiniteNat` `ofSeq_surjective` `isSt_ofSeq_iff_tendsto`
`isSt_inj_real` 📖	—	`IsSt` `ofReal`	—	—	`eq_of_isSt_real`
`isSt_ofSeq_iff_tendsto` 📖	mathematical	—	`IsSt` `ofSeq` `Filter.Tendsto` `Real` `Ultrafilter.toFilter` `Filter.hyperfilter` `instInfiniteNat` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace`	—	`instInfiniteNat` `Iff.and` `ofSeq_lt_ofSeq` `Filter.eventually_and` `Filter.HasBasis.tendsto_right_iff` `nhds_basis_Ioo_pos` `Real.instIsOrderedAddMonoid` `instOrderTopologyReal` `instNoMaxOrderOfNontrivial` `Real.instIsOrderedRing` `Real.instNontrivial`
`isSt_of_tendsto` 📖	mathematical	`Filter.Tendsto` `Real` `Filter.atTop` `Nat.instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace`	`IsSt` `ofSeq`	—	`instInfiniteNat` `isSt_ofSeq_iff_tendsto` `Filter.Tendsto.mono_left` `Nat.hyperfilter_le_atTop`
`isSt_real_iff_eq` 📖	mathematical	—	`IsSt` `ofReal`	—	`eq_of_isSt_real` `isSt_refl_real`
`isSt_refl_real` 📖	mathematical	—	`IsSt` `ofReal`	—	`instInfiniteNat` `isSt_ofSeq_iff_tendsto` `tendsto_const_nhds`
`isSt_sSup` 📖	mathematical	`Infinite`	`IsSt` `SupSet.sSup` `Real` `Real.instSupSet` `setOf` `Hyperreal` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrder` `ofReal`	—	`LT.lt.trans_le` `coe_lt_coe` `sub_one_lt` `Real.instZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `not_lt` `coe_le_coe` `LE.le.trans` `LT.lt.le` `lt_of_not_ge` `LT.lt.not_ge` `sub_lt_self` `csSup_le` `Nat.instAtLeastTwoHAddOfNat` `lt_imp_lt_of_le_of_le` `le_refl` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_zero` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_pf_add_gt` `Nat.cast_one` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Real.instIsOrderedRing` `CancelDenoms.sub_subst` `CancelDenoms.add_subst` `CancelDenoms.div_subst` `Mathlib.Meta.NormNum.isNat_eq_true` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.isNNRat_mul` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `Mathlib.Meta.NormNum.isNat_mul` `Mathlib.Tactic.Linarith.mul_nonpos` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Mathlib.Meta.NormNum.isNat_lt_true` `LE.le.not_gt` `le_csSup` `contravariant_lt_of_covariant_le` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instNontrivial`
`isSt_st` 📖	mathematical	—	`IsSt` `st`	—	`isSt_st'` `Infinite.st_eq`
`isSt_st'` 📖	mathematical	`Infinite`	`IsSt` `st`	—	`IsSt.isSt_st` `isSt_sSup`
`isSt_st_of_exists_st` 📖	mathematical	`IsSt`	`st`	—	`IsSt.isSt_st`
`isSt_symm_real` 📖	mathematical	—	`IsSt` `ofReal`	—	`isSt_real_iff_eq`
`isSt_trans_real` 📖	—	`IsSt` `ofReal`	—	—	`isSt_real_iff_eq`
`lt_neg_of_pos_of_infinitesimal` 📖	mathematical	`Infinitesimal` `Real` `Real.instLT` `Real.instZero`	`Hyperreal` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrder` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `instField` `ofReal`	—	`infinitesimal_def`
`lt_of_pos_of_infinitesimal` 📖	mathematical	`Infinitesimal` `Real` `Real.instLT` `Real.instZero`	`Hyperreal` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrder` `ofReal`	—	`infinitesimal_def`
`lt_of_st_lt` 📖	mathematical	`Infinite` `Real` `Real.instLT` `st`	`Hyperreal` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrder`	—	`IsSt.lt` `isSt_st'`
`lt_of_tendsto_atBot` 📖	mathematical	`Filter.Germ.Tendsto` `Real` `Ultrafilter.toFilter` `Filter.hyperfilter` `instInfiniteNat` `Filter.atBot` `Real.instPreorder`	`Hyperreal` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrder` `ofReal`	—	`instInfiniteNat` `ofSeq_surjective` `ofSeq_lt_ofSeq` `Filter.Tendsto.eventually_mem` `tendsto_ofSeq` `Filter.Iio_mem_atBot` `instNoBotOrderOfNoMinOrder` `instNoMinOrderOfNontrivial` `Real.instIsOrderedRing` `Real.instNontrivial`
`lt_of_tendsto_atTop` 📖	mathematical	`Filter.Germ.Tendsto` `Real` `Ultrafilter.toFilter` `Filter.hyperfilter` `instInfiniteNat` `Filter.atTop` `Real.instPreorder`	`Hyperreal` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrder` `ofReal`	—	`instInfiniteNat` `ofSeq_surjective` `ofSeq_lt_ofSeq` `Filter.Tendsto.eventually_mem` `tendsto_ofSeq` `Filter.Ioi_mem_atTop` `instNoTopOrderOfNoMaxOrder` `instNoMaxOrderOfNontrivial` `Real.instIsOrderedRing` `Real.instNontrivial`
`lt_of_tendsto_zero_of_pos` 📖	mathematical	`Filter.Tendsto` `Real` `Filter.atTop` `Nat.instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instZero` `Real.instLT`	`Hyperreal` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrder` `ofSeq` `ofReal`	—	`instInfiniteNat` `ofSeq_lt_ofSeq` `Filter.Eventually.filter_mono` `Nat.hyperfilter_le_atTop` `Filter.Tendsto.eventually` `gt_mem_nhds` `instOrderTopologyReal`
`neg_lt_of_tendsto_zero_of_pos` 📖	mathematical	`Filter.Tendsto` `Real` `Filter.atTop` `Nat.instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instZero` `Real.instLT`	`Hyperreal` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrder` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `instField` `ofReal` `ofSeq`	—	`Filter.Tendsto.neg` `IsTopologicalRing.toContinuousNeg` `instIsTopologicalRingReal` `neg_lt_of_neg_lt` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `instIsStrictOrderedRing` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `lt_of_tendsto_zero_of_pos` `neg_zero`
`not_infiniteNeg_add_infinitePos` 📖	mathematical	`InfiniteNeg` `InfinitePos`	`Hyperreal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instField`	—	`infinitePos_add_not_infiniteNeg` `add_comm`
`not_infinitePos_add_infiniteNeg` 📖	mathematical	`InfinitePos` `InfiniteNeg`	`Hyperreal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instField`	—	`infiniteNeg_add_not_infinitePos` `add_comm`
`not_infinite_add` 📖	mathematical	`Infinite`	`Hyperreal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instField`	—	`exists_st_of_not_infinite` `not_infinite_of_exists_st` `IsSt.add`
`not_infinite_iff_exist_lt_gt` 📖	mathematical	—	`Infinite` `Hyperreal` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrder` `ofReal`	—	`exists_st_of_not_infinite` `one_pos` `Real.instZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `LT.lt.not_gt`
`not_infinite_mul` 📖	mathematical	`Infinite`	`Hyperreal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instField`	—	`exists_st_of_not_infinite` `IsSt.not_infinite` `IsSt.mul`
`not_infinite_neg` 📖	mathematical	`Infinite`	`Hyperreal` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `instField`	—	`infinite_neg`
`not_infinite_of_exists_st` 📖	mathematical	`IsSt`	`Infinite`	—	`IsSt.not_infinite`
`not_infinite_real` 📖	mathematical	—	`Infinite` `ofReal`	—	`not_infinite_iff_exist_lt_gt` `coe_lt_coe` `sub_one_lt` `Real.instZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `lt_add_one`
`not_infinite_zero` 📖	mathematical	—	`Infinite` `Hyperreal` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instField`	—	`Infinite.ne_zero`
`not_real_of_infinitesimal_ne_zero` 📖	—	`Infinitesimal`	—	—	`coe_eq_zero` `IsSt.unique` `isSt_refl_real`
`ofSeq_le_ofSeq` 📖	mathematical	—	`Hyperreal` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrder` `ofSeq` `Filter.Eventually` `Real` `Real.instLE` `Ultrafilter.toFilter` `Filter.hyperfilter` `instInfiniteNat`	—	`Filter.Germ.coe_le` `instInfiniteNat`
`ofSeq_lt_ofSeq` 📖	mathematical	—	`Hyperreal` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrder` `ofSeq` `Filter.Eventually` `Real` `Real.instLT` `Ultrafilter.toFilter` `Filter.hyperfilter` `instInfiniteNat`	—	`Filter.Germ.coe_lt` `instInfiniteNat`
`ofSeq_surjective` 📖	mathematical	—	`Hyperreal` `ofSeq`	—	`instInfiniteNat`
`omega_ne_zero` 📖	—	—	—	—	`LT.lt.ne'` `omega_pos`
`omega_pos` 📖	mathematical	—	`Hyperreal` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instField` `omega`	—	`coe_lt_omega`
`st_add` 📖	mathematical	`Infinite`	`st` `Hyperreal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instField` `Real` `Real.instAdd`	—	`IsSt.unique` `isSt_st'` `not_infinite_add` `IsSt.add`
`st_eq_sSup` 📖	mathematical	—	`st` `SupSet.sSup` `Real` `Real.instSupSet` `setOf` `Hyperreal` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrder` `ofReal`	—	`em` `Infinite.st_eq` `Set.eq_univ_of_forall` `Real.sSup_univ` `Set.eq_empty_of_forall_notMem` `LT.lt.not_gt` `Membership.mem.out` `Real.sSup_empty` `IsSt.st_eq` `isSt_sSup`
`st_id_real` 📖	mathematical	—	`st` `ofReal`	—	`IsSt.st_eq` `isSt_refl_real`
`st_inv` 📖	mathematical	—	`st` `Hyperreal` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `Field.toSemifield` `instField` `Real` `Real.instInv`	—	`inv_zero` `coe_zero` `st_id_real` `Infinite.st_eq` `infinitesimal_iff_infinite_inv` `IsSt.st_eq` `infinitesimal_inv_of_infinite` `IsSt.inv` `isSt_st'`
`st_le_of_le` 📖	mathematical	`Infinite` `Hyperreal` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrder`	`Real` `Real.instLE` `st`	—	`IsSt.le` `isSt_st'`
`st_mul` 📖	mathematical	`Infinite`	`st` `Hyperreal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instField` `Real` `Real.instMul`	—	`isSt_st'` `not_infinite_mul` `IsSt.unique` `IsSt.mul`
`st_neg` 📖	mathematical	—	`st` `Hyperreal` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `instField` `Real` `Real.instNeg`	—	`Infinite.st_eq` `infinite_neg` `neg_zero` `IsSt.unique` `isSt_st'` `not_infinite_neg` `IsSt.neg`
`stdPart_coe` 📖	mathematical	—	`ArchimedeanClass.stdPart` `Hyperreal` `instLinearOrder` `instField` `IsStrictOrderedRing.toIsOrderedRing` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instIsStrictOrderedRing` `ofReal`	—	`ArchimedeanClass.stdPart_map_real` `IsStrictOrderedRing.toIsOrderedRing` `instIsStrictOrderedRing`
`stdPart_epsilon` 📖	mathematical	—	`ArchimedeanClass.stdPart` `Hyperreal` `instLinearOrder` `instField` `IsStrictOrderedRing.toIsOrderedRing` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instIsStrictOrderedRing` `epsilon` `Real` `Real.instZero`	—	`IsStrictOrderedRing.toIsOrderedRing` `instIsStrictOrderedRing` `IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toIsStrictOrderedRing` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `ArchimedeanClass.stdPart_eq_zero` `LT.lt.ne'` `archimedeanClassMk_epsilon_pos`
`stdPart_of_tendsto` 📖	mathematical	`Filter.Germ.Tendsto` `Real` `Ultrafilter.toFilter` `Filter.hyperfilter` `instInfiniteNat` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace`	`ArchimedeanClass.stdPart` `Hyperreal` `instLinearOrder` `instField` `IsStrictOrderedRing.toIsOrderedRing` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instIsStrictOrderedRing`	—	`instInfiniteNat` `ArchimedeanClass.stdPart_eq` `IsStrictOrderedRing.toIsOrderedRing` `instIsStrictOrderedRing` `tendsto_iff_forall`
`stdPart_omega` 📖	mathematical	—	`ArchimedeanClass.stdPart` `Hyperreal` `instLinearOrder` `instField` `IsStrictOrderedRing.toIsOrderedRing` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instIsStrictOrderedRing` `omega` `Real` `Real.instZero`	—	`IsStrictOrderedRing.toIsOrderedRing` `instIsStrictOrderedRing` `IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toIsStrictOrderedRing` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `ArchimedeanClass.stdPart_eq_zero` `LT.lt.ne` `archimedeanClassMk_omega_neg`
`tendsto_atBot_iff` 📖	mathematical	—	`Filter.Germ.Tendsto` `Real` `Ultrafilter.toFilter` `Filter.hyperfilter` `instInfiniteNat` `Filter.atBot` `Real.instPreorder` `Hyperreal` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instField` `ArchimedeanClass` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `IsOrderedRing.toIsOrderedAddMonoid` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `IsStrictOrderedRing.toIsOrderedRing` `instIsStrictOrderedRing` `ArchimedeanClass.instLinearOrder` `ArchimedeanClass.instZero`	—	`instInfiniteNat` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `instIsStrictOrderedRing` `lt_of_tendsto_atBot` `archimedeanClassMk_neg_of_tendsto_atBot` `ofSeq_surjective` `tendsto_ofSeq` `Filter.tendsto_atBot` `ofSeq_le_ofSeq` `LT.lt.le` `ArchimedeanClass.lt_of_mk_lt_mk_of_nonpos` `LT.lt.trans_le` `archimedeanClassMk_coe_nonneg`
`tendsto_atTop_iff` 📖	mathematical	—	`Filter.Germ.Tendsto` `Real` `Ultrafilter.toFilter` `Filter.hyperfilter` `instInfiniteNat` `Filter.atTop` `Real.instPreorder` `Hyperreal` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instField` `ArchimedeanClass` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `IsOrderedRing.toIsOrderedAddMonoid` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `IsStrictOrderedRing.toIsOrderedRing` `instIsStrictOrderedRing` `ArchimedeanClass.instLinearOrder` `ArchimedeanClass.instZero`	—	`instInfiniteNat` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `instIsStrictOrderedRing` `lt_of_tendsto_atTop` `archimedeanClassMk_neg_of_tendsto_atTop` `ofSeq_surjective` `tendsto_ofSeq` `Filter.tendsto_atTop` `ofSeq_le_ofSeq` `LT.lt.le` `ArchimedeanClass.lt_of_mk_lt_mk_of_nonneg` `LT.lt.trans_le` `archimedeanClassMk_coe_nonneg`
`tendsto_iff_forall` 📖	mathematical	—	`Filter.Germ.Tendsto` `Real` `Ultrafilter.toFilter` `Filter.hyperfilter` `instInfiniteNat` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Hyperreal` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrder` `ofReal`	—	`instInfiniteNat` `ofSeq_surjective` `tendsto_ofSeq` `Filter.HasBasis.tendsto_right_iff` `nhds_basis_Ioo` `instOrderTopologyReal` `instNoMaxOrderOfNontrivial` `Real.instIsOrderedRing` `Real.instNontrivial` `instNoMinOrderOfNontrivial` `NoMaxOrder.exists_gt` `LT.lt.le` `NoMinOrder.exists_lt` `exists_between` `LinearOrderedSemiField.toDenselyOrdered` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `LT.lt.trans_le` `coe_lt_coe` `LE.le.trans_lt`
`tendsto_ofSeq` 📖	mathematical	—	`Filter.Germ.Tendsto` `Real` `Ultrafilter.toFilter` `Filter.hyperfilter` `instInfiniteNat` `ofSeq` `Filter.Tendsto`	—	`instInfiniteNat`

Hyperreal.Infinite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mul` 📖	mathematical	`Hyperreal.Infinite`	`Hyperreal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Hyperreal.instField`	—	`Hyperreal.infinite_mul_of_infinite_not_infinitesimal` `not_infinitesimal`
`ne_real` 📖	—	`Hyperreal.Infinite`	—	—	`Hyperreal.not_infinite_real`
`ne_zero` 📖	—	`Hyperreal.Infinite`	—	—	`LT.lt.ne'` `Hyperreal.InfinitePos.pos` `LT.lt.ne` `Hyperreal.InfiniteNeg.lt_zero`
`not_infinitesimal` 📖	mathematical	`Hyperreal.Infinite`	`Hyperreal.Infinitesimal`	—	`Hyperreal.Infinitesimal.not_infinite`
`st_eq` 📖	mathematical	`Hyperreal.Infinite`	`Hyperreal.st` `Real` `Real.instZero`	—	`Hyperreal.IsSt.not_infinite`

Hyperreal.InfiniteNeg

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`lt_zero` 📖	mathematical	`Hyperreal.InfiniteNeg`	`Hyperreal` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Hyperreal.instLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Hyperreal.instField`	—	—
`neg` 📖	mathematical	`Hyperreal.InfiniteNeg`	`Hyperreal.InfinitePos` `Hyperreal` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `Hyperreal.instField`	—	`lt_neg` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `Hyperreal.instIsStrictOrderedRing` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add`
`not_infinitePos` 📖	mathematical	`Hyperreal.InfiniteNeg`	`Hyperreal.InfinitePos`	—	`LT.lt.not_gt`
`not_infinitesimal` 📖	mathematical	`Hyperreal.InfiniteNeg`	`Hyperreal.Infinitesimal`	—	`Hyperreal.Infinite.not_infinitesimal`

Hyperreal.InfinitePos

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`neg` 📖	mathematical	`Hyperreal.InfinitePos`	`Hyperreal.InfiniteNeg` `Hyperreal` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `Hyperreal.instField`	—	`neg_lt` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `Hyperreal.instIsStrictOrderedRing` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add`
`not_infiniteNeg` 📖	mathematical	`Hyperreal.InfinitePos`	`Hyperreal.InfiniteNeg`	—	`Hyperreal.InfiniteNeg.not_infinitePos`
`not_infinitesimal` 📖	mathematical	`Hyperreal.InfinitePos`	`Hyperreal.Infinitesimal`	—	`Hyperreal.Infinite.not_infinitesimal`
`pos` 📖	mathematical	`Hyperreal.InfinitePos`	`Hyperreal` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Hyperreal.instLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Hyperreal.instField`	—	—

Hyperreal.Infinitesimal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`Hyperreal.Infinitesimal`	`Hyperreal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Hyperreal.instField`	—	`add_zero` `Hyperreal.IsSt.add`
`eq_zero` 📖	mathematical	`Hyperreal.Infinitesimal` `Hyperreal.ofReal`	`Real` `Real.instZero`	—	`Hyperreal.eq_of_isSt_real`
`mul` 📖	mathematical	`Hyperreal.Infinitesimal`	`Hyperreal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Hyperreal.instField`	—	`MulZeroClass.mul_zero` `Hyperreal.IsSt.mul`
`neg` 📖	mathematical	`Hyperreal.Infinitesimal`	`Hyperreal` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `Hyperreal.instField`	—	`neg_zero` `Hyperreal.IsSt.neg`
`not_infinite` 📖	mathematical	`Hyperreal.Infinitesimal`	`Hyperreal.Infinite`	—	`Hyperreal.IsSt.not_infinite`

Hyperreal.IsSt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`Hyperreal.IsSt`	`Hyperreal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Hyperreal.instField` `Real` `Real.instAdd`	—	`map₂` `Continuous.continuousAt` `continuous_add` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal`
`infinitesimal_sub` 📖	mathematical	`Hyperreal.IsSt`	`Hyperreal.Infinitesimal` `Hyperreal` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `Hyperreal.instField` `Hyperreal.ofReal`	—	`sub_self` `sub` `Hyperreal.isSt_refl_real`
`inv` 📖	mathematical	`Hyperreal.Infinitesimal` `Hyperreal.IsSt`	`Hyperreal` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `Field.toSemifield` `Hyperreal.instField` `Real` `Real.instInv`	—	`map` `ContinuousInv₀.continuousAt_inv₀` `IsTopologicalDivisionRing.toContinuousInv₀` `instIsTopologicalDivisionRingReal`
`isSt_st` 📖	mathematical	`Hyperreal.IsSt`	`Hyperreal.st`	—	`st_eq`
`le` 📖	mathematical	`Hyperreal.IsSt` `Hyperreal` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Hyperreal.instLinearOrder`	`Real` `Real.instLE`	—	`not_lt` `LE.le.not_gt` `lt`
`lt` 📖	mathematical	`Hyperreal.IsSt` `Real` `Real.instLT`	`Hyperreal` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Hyperreal.instLinearOrder`	—	`Hyperreal.ofSeq_surjective` `instInfiniteNat` `Hyperreal.ofSeq_lt_ofSeq` `Filter.Tendsto.eventually_lt` `OrderTopology.to_orderClosedTopology` `instOrderTopologyReal` `Hyperreal.isSt_ofSeq_iff_tendsto`
`map` 📖	mathematical	`Hyperreal.IsSt` `ContinuousAt` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace`	`Filter.Germ.map` `Ultrafilter.toFilter` `Filter.hyperfilter` `instInfiniteNat`	—	`instInfiniteNat` `Hyperreal.ofSeq_surjective` `Hyperreal.isSt_ofSeq_iff_tendsto` `Filter.Tendsto.comp` `ContinuousAt.tendsto`
`map₂` 📖	mathematical	`Hyperreal.IsSt` `ContinuousAt` `Real` `instTopologicalSpaceProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace`	`Filter.Germ.map₂` `Ultrafilter.toFilter` `Filter.hyperfilter` `instInfiniteNat`	—	`instInfiniteNat` `Hyperreal.ofSeq_surjective` `Hyperreal.isSt_ofSeq_iff_tendsto` `Filter.Tendsto.comp` `ContinuousAt.tendsto` `Filter.Tendsto.prodMk_nhds`
`mul` 📖	mathematical	`Hyperreal.IsSt`	`Hyperreal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Hyperreal.instField` `Real` `Real.instMul`	—	`map₂` `Continuous.continuousAt` `continuous_mul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal`
`neg` 📖	mathematical	`Hyperreal.IsSt`	`Hyperreal` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `Hyperreal.instField` `Real` `Real.instNeg`	—	`map` `Continuous.continuousAt` `ContinuousNeg.continuous_neg` `IsTopologicalRing.toContinuousNeg` `instIsTopologicalRingReal`
`not_infinite` 📖	mathematical	`Hyperreal.IsSt`	`Hyperreal.Infinite`	—	`lt_asymm` `one_pos` `Real.instZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing`
`st_eq` 📖	mathematical	`Hyperreal.IsSt`	`Hyperreal.st`	—	`Hyperreal.st.eq_1` `unique`
`sub` 📖	mathematical	`Hyperreal.IsSt`	`Hyperreal` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `Hyperreal.instField` `Real` `Real.instSub`	—	`map₂` `Continuous.continuousAt` `ContinuousSub.continuous_sub` `IsTopologicalAddGroup.to_continuousSub` `instIsTopologicalAddGroupReal`
`unique` 📖	—	`Hyperreal.IsSt`	—	—	`Hyperreal.ofSeq_surjective` `tendsto_nhds_unique` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `instInfiniteNat` `Ultrafilter.neBot` `Hyperreal.isSt_ofSeq_iff_tendsto`

---

← Back to Index