Field

📁 Source: Mathlib/Topology/Algebra/Order/Field.lean

Statistics

Metric	Count
Definitions Field	1
Theorems atBot_mul_neg, atBot_mul_pos, atTop_mul_neg, atTop_mul_pos, const_div_atBot, const_div_atTop, div_atBot, div_atTop, inv_tendsto_atBot, inv_tendsto_atTop, inv_tendsto_nhdsGT_zero, inv_tendsto_nhdsLT_zero, neg_mul_atBot, neg_mul_atTop, pos_mul_atBot, pos_mul_atTop, toContinuousInv₀, toHasContinuousInv₀, toIsTopologicalDivisionRing, topologicalRing, of_norm, bdd_le_mul_tendsto_zero, bdd_le_mul_tendsto_zero', comap_mulLeft_nhdsGT_zero, eventually_nhdsGT_zero_mul_left, inv_atBot₀, inv_atTop₀, inv_nhdsGT_zero, inv_nhdsLT_zero, tendsto_bdd_div_atTop_nhds_zero, tendsto_const_mul_pow_nhds_iff, tendsto_const_mul_pow_nhds_iff', tendsto_const_mul_zpow_atTop_nhds_iff, tendsto_const_mul_zpow_atTop_zero, tendsto_inv_atBot_nhdsLT_zero, tendsto_inv_atBot_zero, tendsto_inv_atTop_nhdsGT_zero, tendsto_inv_atTop_zero, tendsto_inv_nhdsGT_zero, tendsto_inv_nhdsLT_zero, tendsto_nhdsGT_zero_of_comp_inv_tendsto_atTop, tendsto_nhdsLT_zero_of_comp_inv_tendsto_atBot, tendsto_pow_neg_atTop, tendsto_zpow_atTop_zero	44
Total	45

Filter.Tendsto

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
atBot_mul_neg 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Filter.Tendsto Filter.atBot nhds	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Filter.atTop	—	atTop_mul_neg comp Filter.tendsto_neg_atBot_atTop IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing neg_mul neg_neg
atBot_mul_pos 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Filter.Tendsto Filter.atBot nhds	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	atTop_mul_pos comp Filter.tendsto_neg_atBot_atTop IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing neg_mul neg_neg Filter.tendsto_neg_atTop_atBot
atTop_mul_neg 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Filter.Tendsto Filter.atTop nhds	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Filter.atBot	—	atTop_mul_pos neg_pos IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing neg IsTopologicalRing.toContinuousNeg IsStrictOrderedRing.topologicalRing neg_mul_eq_mul_neg neg_neg comp Filter.tendsto_neg_atTop_atBot
atTop_mul_pos 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Filter.Tendsto Filter.atTop nhds	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	Filter.tendsto_atTop_mono' Nat.instAtLeastTwoHAddOfNat Filter.mp_mem eventually_ge_atTop eventually lt_mem_nhds half_lt_self PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Filter.univ_mem' mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono IsStrictOrderedRing.toIsOrderedRing LT.lt.le atTop_mul_const half_pos
const_div_atBot 📖	mathematical	Filter.Tendsto Filter.atBot PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing nhds MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	—	div_atBot tendsto_const_nhds
const_div_atTop 📖	mathematical	Filter.Tendsto Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing nhds MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	—	div_atTop tendsto_const_nhds
div_atBot 📖	mathematical	Filter.Tendsto nhds Filter.atBot PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	—	div_eq_mul_inv mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsStrictOrderedRing.topologicalRing comp tendsto_inv_atBot_zero MulZeroClass.mul_zero
div_atTop 📖	mathematical	Filter.Tendsto nhds Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	—	div_eq_mul_inv mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsStrictOrderedRing.topologicalRing comp tendsto_inv_atTop_zero MulZeroClass.mul_zero
inv_tendsto_atBot 📖	mathematical	Filter.Tendsto Filter.atBot PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Pi.instInv InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero Field.toSemifield nhds MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	—	comp tendsto_inv_atBot_zero
inv_tendsto_atTop 📖	mathematical	Filter.Tendsto Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Pi.instInv InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero nhds MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring	—	comp tendsto_inv_atTop_zero
inv_tendsto_nhdsGT_zero 📖	mathematical	Filter.Tendsto nhdsWithin MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Set.Ioi PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Pi.instInv InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero Filter.atTop	—	comp tendsto_inv_nhdsGT_zero
inv_tendsto_nhdsLT_zero 📖	mathematical	Filter.Tendsto nhdsWithin MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Set.Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Pi.instInv InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero Field.toSemifield Filter.atBot	—	comp tendsto_inv_nhdsLT_zero
neg_mul_atBot 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Filter.Tendsto nhds Filter.atBot	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Filter.atTop	—	mul_comm atBot_mul_neg
neg_mul_atTop 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Filter.Tendsto nhds Filter.atTop	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Filter.atBot	—	mul_comm atTop_mul_neg
pos_mul_atBot 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Filter.Tendsto nhds Filter.atBot	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	mul_comm atBot_mul_pos
pos_mul_atTop 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Filter.Tendsto nhds Filter.atTop	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	mul_comm atTop_mul_pos

IsStrictOrderedRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toContinuousInv₀ 📖	mathematical	—	ContinuousInv₀ MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero	—	ContinuousInv₀.of_nhds_one tendsto_order Nat.instAtLeastTwoHAddOfNat LT.lt.trans_le one_half_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE toPosMulStrictMono le_max_right le_max_left max_lt one_half_lt_one Filter.mp_mem Ioo_mem_nhds OrderTopology.to_orderClosedTopology one_pos toZeroLEOneClass NeZero.charZero_one toCharZero one_lt_inv₀ Filter.univ_mem' LE.le.trans_lt lt_inv_of_lt_inv₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE toMulPosStrictMono Ioi_mem_nhds instClosedIicTopology inv_lt_one_of_one_lt₀ inv_lt_of_inv_lt₀ lt_trans Mathlib.Meta.Positivity.pos_of_isNat toIsOrderedRing instNontrivialOfCharZero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one
toHasContinuousInv₀ 📖	mathematical	—	ContinuousInv₀ MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero	—	toContinuousInv₀
toIsTopologicalDivisionRing 📖	mathematical	—	IsTopologicalDivisionRing Field.toDivisionRing	—	topologicalRing toContinuousInv₀ IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring
topologicalRing 📖	mathematical	—	IsTopologicalRing NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	—	IsTopologicalRing.of_norm LinearOrderedAddCommGroup.toIsTopologicalAddGroup IsOrderedRing.toIsOrderedAddMonoid toIsOrderedRing abs_nonneg IsOrderedAddMonoid.toAddLeftMono covariant_swap_add_of_covariant_add Eq.le abs_mul sub_zero nhds_basis_abs_sub_lt instNoMaxOrderOfNontrivial instNontrivialOfCharZero toCharZero

IsTopologicalRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_norm 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Filter.HasBasis nhds Preorder.toLT setOf	IsTopologicalRing	—	Filter.HasBasis.tendsto_iff exists_pos_mul_lt LE.le.trans_lt mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono IsStrictOrderedRing.toIsOrderedRing le_of_lt of_addGroup_of_nhds_zero Filter.HasBasis.prod one_pos IsStrictOrderedRing.toZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero mul_le_of_le_one_left IsOrderedRing.toMulPosMono LT.lt.le LE.le.trans_eq mul_comm

(root)

Definitions

Name	Category	Theorems
Field 📖	CompData	3 math math: Field.nonempty_iff, Fintype.nonempty_field_iff, Infinite.nonempty_field

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bdd_le_mul_tendsto_zero 📖	mathematical	Filter.Eventually Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Filter.Tendsto nhds MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	neg_le IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing covariant_swap_add_of_covariant_add le_max_of_le_left neg_le_abs le_max_of_le_right le_abs_self bdd_le_mul_tendsto_zero' Filter.mp_mem Filter.univ_mem' abs_le LE.le.trans
bdd_le_mul_tendsto_zero' 📖	mathematical	Filter.Eventually Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder abs AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing Filter.Tendsto nhds MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	tendsto_zero_iff_abs_tendsto_zero IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing MulZeroClass.mul_zero abs_zero IsOrderedAddMonoid.toAddLeftMono Filter.Tendsto.abs Filter.Tendsto.const_mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsStrictOrderedRing.topologicalRing tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds Filter.mp_mem Filter.univ_mem' abs_nonneg covariant_swap_add_of_covariant_add abs_mul mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono LE.le.trans le_abs_self
comap_mulLeft_nhdsGT_zero 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	Filter.comap Distrib.toMul NonUnitalNonAssocSemiring.toDistrib nhdsWithin Set.Ioi	—	nhdsWithin.eq_1 Filter.comap_inf Filter.comap_principal Set.preimage_const_mul_Ioi₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono zero_div IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing IsStrictOrderedRing.toIsTopologicalDivisionRing LT.lt.ne' Homeomorph.comap_nhds_eq MulZeroClass.mul_zero
eventually_nhdsGT_zero_mul_left 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Filter.Eventually nhdsWithin Set.Ioi	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	comap_mulLeft_nhdsGT_zero Filter.Eventually.comap
inv_atBot₀ 📖	mathematical	—	Filter Filter.instInv InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero Field.toSemifield Filter.atBot PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder nhdsWithin MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Set.Iio	—	Filter.HasBasis.eq_of_same_basis Filter.HasBasis.comp_surjective Filter.HasBasis.map Filter.atBot_basis_Iio' SemilatticeInf.instIsCodirectedOrder instNoMinOrderOfNontrivial IsStrictOrderedRing.toIsOrderedRing instNontrivialOfCharZero IsStrictOrderedRing.toCharZero inv_surjective Filter.HasBasis.congr nhdsLT_basis IsOrderedRing.toPosMulMono Set.image_inv_eq_inv Set.inv_Iio₀ inv_neg'' inv_inv
inv_atTop₀ 📖	mathematical	—	Filter Filter.instInv InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder nhdsWithin MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Set.Ioi	—	Filter.HasBasis.eq_of_same_basis Filter.HasBasis.comp_surjective Filter.HasBasis.map Filter.atTop_basis_Ioi' SemilatticeSup.instIsDirectedOrder IsStrictOrderedRing.toNoMaxOrder inv_surjective Filter.HasBasis.congr nhdsGT_basis PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Set.image_inv_eq_inv Set.inv_Ioi₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono inv_pos inv_inv
inv_nhdsGT_zero 📖	mathematical	—	Filter Filter.instInv InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero nhdsWithin MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Set.Ioi PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Filter.atTop	—	inv_atTop₀ inv_inv
inv_nhdsLT_zero 📖	mathematical	—	Filter Filter.instInv InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero Field.toSemifield nhdsWithin MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Set.Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Filter.atBot	—	inv_atBot₀ inv_inv
tendsto_bdd_div_atTop_nhds_zero 📖	mathematical	Filter.Eventually Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Filter.Tendsto Filter.atTop	DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing nhds MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	—	div_eq_mul_inv bdd_le_mul_tendsto_zero Filter.Tendsto.inv_tendsto_atTop
tendsto_const_mul_pow_nhds_iff 📖	mathematical	—	Filter.Tendsto Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder nhds	—	—
tendsto_const_mul_pow_nhds_iff' 📖	mathematical	—	Filter.Tendsto Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder nhds MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	eq_or_ne pow_zero mul_one T2Space.t1Space OrderClosedTopology.to_t2Space OrderTopology.to_orderClosedTopology Filter.atTop_neBot SemilatticeSup.instIsDirectedOrder Nontrivial.to_nonempty instNontrivialOfCharZero IsStrictOrderedRing.toCharZero lt_trichotomy Filter.tendsto_const_mul_pow_atBot_iff not_tendsto_nhds_of_tendsto_atBot instNoBotOrderOfNoMinOrder instNoMinOrderOfNontrivial IsStrictOrderedRing.toIsOrderedRing instClosedIicTopology LT.lt.ne MulZeroClass.zero_mul Filter.tendsto_const_mul_pow_atTop_iff not_tendsto_nhds_of_tendsto_atTop instNoTopOrderOfNoMaxOrder instNoMaxOrderOfNontrivial instClosedIciTopology LT.lt.ne'
tendsto_const_mul_zpow_atTop_nhds_iff 📖	mathematical	—	Filter.Tendsto Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing DivInvMonoid.toZPow DivisionRing.toDivInvMonoid Field.toDivisionRing Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder nhds MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	zpow_natCast tendsto_const_mul_pow_nhds_iff tendsto_nhds_unique OrderClosedTopology.to_t2Space OrderTopology.to_orderClosedTopology Filter.atTop_neBot SemilatticeSup.instIsDirectedOrder Nontrivial.to_nonempty instNontrivialOfCharZero IsStrictOrderedRing.toCharZero tendsto_const_mul_zpow_atTop_zero zpow_zero mul_one tendsto_const_nhds
tendsto_const_mul_zpow_atTop_zero 📖	mathematical	—	Filter.Tendsto Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing DivInvMonoid.toZPow DivisionRing.toDivInvMonoid Field.toDivisionRing Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder nhds MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	Filter.Tendsto.const_mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsStrictOrderedRing.topologicalRing tendsto_zpow_atTop_zero MulZeroClass.mul_zero
tendsto_inv_atBot_nhdsLT_zero 📖	mathematical	—	Filter.Tendsto InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero Field.toSemifield Filter.atBot PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder nhdsWithin MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Set.Iio	—	Eq.le inv_atBot₀
tendsto_inv_atBot_zero 📖	mathematical	—	Filter.Tendsto InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero Field.toSemifield Filter.atBot PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder nhds MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	—	Filter.Tendsto.mono_right tendsto_inv_atBot_nhdsLT_zero inf_le_left
tendsto_inv_atTop_nhdsGT_zero 📖	mathematical	—	Filter.Tendsto InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder nhdsWithin MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Set.Ioi	—	Eq.le inv_atTop₀
tendsto_inv_atTop_zero 📖	mathematical	—	Filter.Tendsto InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder nhds MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring	—	Filter.Tendsto.mono_right tendsto_inv_atTop_nhdsGT_zero inf_le_left
tendsto_inv_nhdsGT_zero 📖	mathematical	—	Filter.Tendsto InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero nhdsWithin MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Set.Ioi PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Filter.atTop	—	Eq.le inv_nhdsGT_zero
tendsto_inv_nhdsLT_zero 📖	mathematical	—	Filter.Tendsto InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero Field.toSemifield nhdsWithin MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Set.Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Filter.atBot	—	Eq.le inv_nhdsLT_zero
tendsto_nhdsGT_zero_of_comp_inv_tendsto_atTop 📖	mathematical	Filter.Tendsto InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	nhdsWithin MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Set.Ioi	—	Filter.Tendsto.comp tendsto_inv_nhdsGT_zero
tendsto_nhdsLT_zero_of_comp_inv_tendsto_atBot 📖	mathematical	Filter.Tendsto InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero Field.toSemifield Filter.atBot PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	nhdsWithin MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Set.Iio	—	Filter.Tendsto.comp tendsto_inv_nhdsLT_zero
tendsto_pow_neg_atTop 📖	mathematical	—	Filter.Tendsto DivInvMonoid.toZPow GroupWithZero.toDivInvMonoid DivisionSemiring.toGroupWithZero Semifield.toDivisionSemiring Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder nhds MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring	—	zpow_neg zpow_natCast Filter.Tendsto.inv_tendsto_atTop Filter.tendsto_pow_atTop IsStrictOrderedRing.toIsOrderedRing
tendsto_zpow_atTop_zero 📖	mathematical	—	Filter.Tendsto DivInvMonoid.toZPow GroupWithZero.toDivInvMonoid DivisionSemiring.toGroupWithZero Semifield.toDivisionSemiring Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder nhds MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring	—	CanLift.prf instCanLiftIntNatCastLeOfNat le_of_lt neg_pos IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd Int.instAddLeftMono neg_neg tendsto_pow_neg_atTop LT.lt.ne' Nat.cast_pos IsStrictOrderedRing.toIsOrderedRing Int.instIsStrictOrderedRing Int.instNontrivial

---

← Back to Index