Documentation Verification Report

Lemmas

📁 Source: Mathlib/Analysis/Normed/Field/Lemmas.lean

Statistics

Metric	Count
Definitions `mulLeft`, `mulRight`, `instDenselyNormedField`, `instNormedField`	4
Theorems `mulLeft_apply`, `mulLeft_symm_apply`, `mulRight_apply`, `mulRight_symm_apply`, `inv_cobounded₀`, `inv_nhdsNE_zero`, `inv_nhdsWithin_ne_zero`, `map_mul_left_cobounded`, `map_mul_right_cobounded`, `tendsto_inv₀_cobounded`, `tendsto_inv₀_cobounded'`, `tendsto_inv₀_nhdsNE_zero`, `tendsto_inv₀_nhdsWithin_ne_zero`, `tendsto_mul_left_cobounded`, `tendsto_mul_right_cobounded`, `to_continuousInv₀`, `to_hasContinuousInv₀`, `to_isTopologicalDivisionRing`, `completeSpace_iff_isComplete_closedBall`, `continuousAt_inv`, `continuousAt_zpow`, `denseRange_nnnorm`, `discreteTopology_of_bddAbove_range_norm`, `discreteTopology_or_nontriviallyNormedField`, `tendsto_norm_inv_nhdsNE_zero_atTop`, `tendsto_norm_zpow_nhdsNE_zero_atTop`, `div₀`, `fun_div₀`, `fun_inv₀`, `fun_inv₀_of_disjoint`, `inv₀`, `inv₀_of_disjoint`, `div₀`, `fun_div₀`, `fun_inv₀`, `fun_inv₀_of_disjoint`, `inv₀`, `inv₀_of_disjoint`, `fun_inv₀`, `inv₀`, `fun_inv₀`, `inv₀`, `tendsto_norm_inv_nhdsNE_zero_atTop`, `tendsto_zpow_nhdsNE_zero_cobounded`, `uniformContinuousOn_inv₀`	45
Total	49

DilationEquiv

Definitions

Name	Category	Theorems
`mulLeft` 📖	CompOp	2 math math: `mulLeft_symm_apply`, `mulLeft_apply`
`mulRight` 📖	CompOp	2 math math: `mulRight_symm_apply`, `mulRight_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mulLeft_apply` 📖	mathematical	—	`DFunLike.coe` `DilationEquiv` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedDivisionRing.toMetricSpace` `EquivLike.toFunLike` `instEquivLike` `mulLeft` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `DivisionSemiring.toGroupWithZero` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing`	—	—
`mulLeft_symm_apply` 📖	mathematical	—	`DFunLike.coe` `DilationEquiv` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedDivisionRing.toMetricSpace` `EquivLike.toFunLike` `instEquivLike` `symm` `mulLeft` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `DivisionSemiring.toGroupWithZero` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing` `DivInvMonoid.toInv` `DivisionMonoid.toDivInvMonoid` `GroupWithZero.toDivisionMonoid`	—	`Units.val_inv_eq_inv_val`
`mulRight_apply` 📖	mathematical	—	`DFunLike.coe` `DilationEquiv` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedDivisionRing.toMetricSpace` `EquivLike.toFunLike` `instEquivLike` `mulRight` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `DivisionSemiring.toGroupWithZero` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing`	—	—
`mulRight_symm_apply` 📖	mathematical	—	`DFunLike.coe` `DilationEquiv` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedDivisionRing.toMetricSpace` `EquivLike.toFunLike` `instEquivLike` `symm` `mulRight` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `DivisionSemiring.toGroupWithZero` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing` `DivInvMonoid.toInv` `DivisionMonoid.toDivInvMonoid` `GroupWithZero.toDivisionMonoid`	—	`Units.val_inv_eq_inv_val`

Filter

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`inv_cobounded₀` 📖	mathematical	—	`Filter` `instInv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid` `DivisionSemiring.toGroupWithZero` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing` `Bornology.cobounded` `PseudoMetricSpace.toBornology` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet`	—	`comap_norm_atTop` `comap_inv` `comap_norm_nhdsGT_zero` `inv_atTop₀` `Real.instIsStrictOrderedRing` `instOrderTopologyReal` `comap_comap` `norm_inv`
`inv_nhdsNE_zero` 📖	mathematical	—	`Filter` `instInv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid` `DivisionSemiring.toGroupWithZero` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet` `Bornology.cobounded` `PseudoMetricSpace.toBornology`	—	`inv_cobounded₀` `inv_inv`
`inv_nhdsWithin_ne_zero` 📖	mathematical	—	`Filter` `instInv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid` `DivisionSemiring.toGroupWithZero` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet` `Bornology.cobounded` `PseudoMetricSpace.toBornology`	—	`inv_nhdsNE_zero`
`map_mul_left_cobounded` 📖	mathematical	—	`map` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `NormedDivisionRing.toNormedRing` `Bornology.cobounded` `PseudoMetricSpace.toBornology` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing`	—	`DilationEquiv.map_cobounded` `DilationEquiv.instDilationEquivClass`
`map_mul_right_cobounded` 📖	mathematical	—	`map` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `NormedDivisionRing.toNormedRing` `Bornology.cobounded` `PseudoMetricSpace.toBornology` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing`	—	`DilationEquiv.map_cobounded` `DilationEquiv.instDilationEquivClass`
`tendsto_inv₀_cobounded` 📖	mathematical	—	`Tendsto` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid` `DivisionSemiring.toGroupWithZero` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing` `Bornology.cobounded` `PseudoMetricSpace.toBornology` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing`	—	`Tendsto.mono_right` `tendsto_inv₀_cobounded'` `inf_le_left`
`tendsto_inv₀_cobounded'` 📖	mathematical	—	`Tendsto` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid` `DivisionSemiring.toGroupWithZero` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing` `Bornology.cobounded` `PseudoMetricSpace.toBornology` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet`	—	`Eq.le` `inv_cobounded₀`
`tendsto_inv₀_nhdsNE_zero` 📖	mathematical	—	`Tendsto` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid` `DivisionSemiring.toGroupWithZero` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet` `Bornology.cobounded` `PseudoMetricSpace.toBornology`	—	`Eq.le` `inv_nhdsNE_zero`
`tendsto_inv₀_nhdsWithin_ne_zero` 📖	mathematical	—	`Tendsto` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid` `DivisionSemiring.toGroupWithZero` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet` `Bornology.cobounded` `PseudoMetricSpace.toBornology`	—	`tendsto_inv₀_nhdsNE_zero`
`tendsto_mul_left_cobounded` 📖	mathematical	—	`Tendsto` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `NormedDivisionRing.toNormedRing` `Bornology.cobounded` `PseudoMetricSpace.toBornology` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing`	—	`Eq.le` `map_mul_left_cobounded`
`tendsto_mul_right_cobounded` 📖	mathematical	—	`Tendsto` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `NormedDivisionRing.toNormedRing` `Bornology.cobounded` `PseudoMetricSpace.toBornology` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing`	—	`Eq.le` `map_mul_right_cobounded`

NormedDivisionRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`to_continuousInv₀` 📖	mathematical	—	`ContinuousInv₀` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `toNormedRing` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid` `DivisionSemiring.toGroupWithZero` `DivisionRing.toDivisionSemiring` `toDivisionRing` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing`	—	`ContinuousOn.continuousAt` `Nat.instAtLeastTwoHAddOfNat` `UniformContinuousOn.continuousOn` `uniformContinuousOn_inv₀` `IsOpen.mem_nhds` `IsClosed.isOpen_compl` `Metric.isClosed_closedBall` `dist_zero` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Metric.closedBall_mem_nhds` `Real.instIsOrderedRing` `Real.instNontrivial`
`to_hasContinuousInv₀` 📖	mathematical	—	`ContinuousInv₀` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `toNormedRing` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid` `DivisionSemiring.toGroupWithZero` `DivisionRing.toDivisionSemiring` `toDivisionRing` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing`	—	`to_continuousInv₀`
`to_isTopologicalDivisionRing` 📖	mathematical	—	`IsTopologicalDivisionRing` `toDivisionRing` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `toNormedRing`	—	`NonUnitalSeminormedRing.toIsTopologicalRing` `to_continuousInv₀`

NormedField

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`completeSpace_iff_isComplete_closedBall` 📖	mathematical	—	`CompleteSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `toNormedCommRing` `IsComplete` `Metric.closedBall` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `Real` `Real.instOne`	—	`IsClosed.isComplete` `Metric.isClosed_closedBall` `discreteTopology_or_nontriviallyNormedField` `completeSpace_iff_isComplete_univ` `NormedDivisionRing.unitClosedBall_eq_univ_of_discrete` `Metric.complete_of_cauchySeq_tendsto` `CauchySeq.norm_bddAbove` `LE.le.trans` `norm_nonneg` `exists_lt_norm` `UniformContinuous.comp_cauchySeq` `uniformContinuous_div_const'` `Ring.uniformContinuousConstSMul_op` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `dist_zero_right` `norm_div` `div_le_one` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `LE.le.trans_lt` `LE.le.trans'` `LT.lt.le` `cauchySeq_tendsto_of_isComplete` `Filter.Tendsto.congr` `Mathlib.Tactic.Contrapose.contrapose₃` `norm_zero` `div_mul_cancel₀` `Filter.Tendsto.comp` `Continuous.tendsto` `continuous_mul_right`
`continuousAt_inv` 📖	mathematical	—	`ContinuousAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `toNormedCommRing` `NontriviallyNormedField.toNormedField` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `Field.toSemifield` `toField`	—	`zpow_neg` `zpow_one` `continuousAt_zpow`
`continuousAt_zpow` 📖	mathematical	—	`ContinuousAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `toNormedCommRing` `NontriviallyNormedField.toNormedField` `DivInvMonoid.toZPow` `DivisionRing.toDivInvMonoid` `NormedDivisionRing.toDivisionRing` `toNormedDivisionRing`	—	`Mathlib.Tactic.Contrapose.contrapose₁` `Filter.Tendsto.not_tendsto` `Filter.Tendsto.mono_left` `ContinuousAt.tendsto` `nhdsWithin_le_nhds` `nhdsNE_neBot` `Metric.disjoint_nhds_cobounded` `tendsto_zpow_nhdsNE_zero_cobounded` `continuousAt_zpow₀` `IsTopologicalDivisionRing.toContinuousInv₀` `NormedDivisionRing.to_isTopologicalDivisionRing` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing`
`denseRange_nnnorm` 📖	mathematical	—	`DenseRange` `NNReal` `NNReal.instTopologicalSpace` `NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `toNormedCommRing` `DenselyNormedField.toNormedField`	—	`dense_of_exists_between` `NNReal.instOrderTopology` `exists_lt_nnnorm_lt`
`discreteTopology_of_bddAbove_range_norm` 📖	mathematical	`BddAbove` `Real` `Real.instLE` `Set.range` `Norm.norm` `toNorm`	`DiscreteTopology` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `toNormedCommRing`	—	`discreteTopology_or_nontriviallyNormedField` `exists_lt_norm` `LT.lt.not_ge` `Set.mem_range_self`
`discreteTopology_or_nontriviallyNormedField` 📖	mathematical	—	`DiscreteTopology` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `toNormedCommRing` `NontriviallyNormedField` `NormedField` `NontriviallyNormedField.toNormedField`	—	`IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `dist_eq_norm` `sub_zero` `zero_lt_one` `Real.instZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `Mathlib.Tactic.Contrapose.contrapose₂` `Mathlib.Tactic.Push.not_forall_eq`
`tendsto_norm_inv_nhdsNE_zero_atTop` 📖	mathematical	—	`Filter.Tendsto` `Real` `Norm.norm` `NormedDivisionRing.toNorm` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid` `DivisionSemiring.toGroupWithZero` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet` `Filter.atTop` `Real.instPreorder`	—	`tendsto_norm_inv_nhdsNE_zero_atTop`
`tendsto_norm_zpow_nhdsNE_zero_atTop` 📖	mathematical	—	`Filter.Tendsto` `Real` `Norm.norm` `NormedDivisionRing.toNorm` `DivInvMonoid.toZPow` `DivisionRing.toDivInvMonoid` `NormedDivisionRing.toDivisionRing` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet` `Filter.atTop` `Real.instPreorder`	—	`Filter.Tendsto.comp` `tendsto_norm_cobounded_atTop` `tendsto_zpow_nhdsNE_zero_cobounded`

Rat

Definitions

Name	Category	Theorems
`instDenselyNormedField` 📖	CompOp	—
`instNormedField` 📖	CompOp	58 math math: `PadicInt.isCauSeq_nthHom`, `Padic.withValUniformEquiv_norm_le_one_iff`, `NumberField.norm_norm_le_norm_mul_house_pow`, `padicValuation_cast`, `PadicSeq.ne_zero_iff_nequiv_zero`, `Padic.exi_rat_seq_conv_cauchy`, `padicValuation_self`, `IsIntegralClosure.intEquiv_apply_eq_ringOfIntegersEquiv`, `Padic.zero_def`, `IsCyclotomicExtension.Rat.cyclotomicRing_isIntegralClosure_of_prime_pow`, `IsIntegral.ratCast_iff`, `padicNormE.defn`, `NumberField.InfinitePlace.map_ratCast`, `Padic.comap_mulValuation_eq_padicValuation`, `IsCyclotomicExtension.Rat.cyclotomicRing_isIntegralClosure`, `PadicSeq.norm_neg`, `NumberField.hermiteTheorem.finite_of_discr_bdd_of_isComplex`, `PadicSeq.norm_nonarchimedean`, `PadicSeq.not_equiv_zero_const_of_nonzero`, `Polynomial.cyclotomic.isCoprime_rat`, `PadicInt.nthHomSeq_mul`, `Padic.mk_eq`, `Padic.toEquiv_withValUniformEquiv_eq_toEquiv_withValRingEquiv`, `NumberField.finite_of_discr_bdd`, `PadicSeq.not_limZero_const_of_nonzero`, `padicValuation_eq_zero_iff`, `Polynomial.cyclotomic_eq_minpoly_rat`, `NumberField.canonicalEmbedding.mem_rat_span_latticeBasis`, `NumberField.Embeddings.coeff_bdd_of_norm_le`, `hahnEmbedding_isOrderedModule_rat`, `NumberField.linearDisjoint_of_isGalois_isCoprime_discr`, `cosetToCuspOrbit_apply_mk`, `Polynomial.X_pow_sub_X_sub_one_irreducible_rat`, `Padic.withValUniformEquiv_cast_apply`, `Padic.coe_withValRingEquiv`, `Padic.isUniformInducing_cast_withVal`, `Polynomial.cyclotomic.irreducible_rat`, `IsCyclotomicExtension.Rat.cyclotomicRing_isIntegralClosure_of_prime`, `PadicSeq.add_eq_max_of_ne`, `PadicInt.isCauSeq_padicNorm_of_pow_dvd_sub`, `Padic.coe_withValRingEquiv_symm`, `PadicInt.nthHomSeq_add`, `Polynomial.Gal.card_complex_roots_eq_card_real_add_card_not_gal_inv`, `Padic.norm_rat_le_one_iff_padicValuation_le_one`, `surjective_padicValuation`, `PadicInt.nthHomSeq_one`, `PadicSeq.norm_const`, `PadicSeq.norm_one`, `PadicSeq.norm_zero_iff`, `instNonemptySeedRatReal`, `PadicSeq.norm_mul`, `Padic.const_equiv`, `Padic.isDenseInducing_cast_withVal`, `PadicSeq.eq_zero_iff_equiv_zero`, `NumberField.mixedEmbedding.mem_rat_span_latticeBasis`, `padicValuation_le_one_iff`, `niven_fract_angle_div_pi_eq`, `NumberField.hermiteTheorem.finite_of_discr_bdd_of_isReal`

TendstoLocallyUniformly

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`div₀` 📖	mathematical	`TendstoLocallyUniformly` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `Continuous` `UniformSpace.toTopologicalSpace`	`Pi.instDiv` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `NormedDivisionRing.toDivisionRing`	—	`div_eq_mul_inv` `mul₀` `NormSMulClass.toIsBoundedSMul` `NormMulClass.toNormSMulClass` `NormedDivisionRing.toNormMulClass` `inv₀` `Continuous.inv₀` `NormedDivisionRing.to_continuousInv₀`
`fun_div₀` 📖	mathematical	`TendstoLocallyUniformly` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `Continuous` `UniformSpace.toTopologicalSpace`	`DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `NormedDivisionRing.toDivisionRing`	—	`div₀`
`fun_inv₀` 📖	mathematical	`TendstoLocallyUniformly` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `Continuous` `UniformSpace.toTopologicalSpace`	`InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid` `DivisionSemiring.toGroupWithZero` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing`	—	`inv₀`
`fun_inv₀_of_disjoint` 📖	mathematical	`TendstoLocallyUniformly` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `Disjoint` `Filter` `Filter.instPartialOrder` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteLattice.toBoundedOrder` `Filter.instCompleteLatticeFilter` `Filter.map` `nhds` `UniformSpace.toTopologicalSpace` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing`	`InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid` `DivisionSemiring.toGroupWithZero` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing`	—	`inv₀_of_disjoint`
`inv₀` 📖	mathematical	`TendstoLocallyUniformly` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `Continuous` `UniformSpace.toTopologicalSpace`	`Pi.instInv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid` `DivisionSemiring.toGroupWithZero` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing`	—	`inv₀_of_disjoint` `Disjoint.mono_left` `Continuous.tendsto` `disjoint_nhds_nhds` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace`
`inv₀_of_disjoint` 📖	mathematical	`TendstoLocallyUniformly` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `Disjoint` `Filter` `Filter.instPartialOrder` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteLattice.toBoundedOrder` `Filter.instCompleteLatticeFilter` `Filter.map` `nhds` `UniformSpace.toTopologicalSpace` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing`	`Pi.instInv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid` `DivisionSemiring.toGroupWithZero` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing`	—	`tendstoLocallyUniformlyOn_univ` `TendstoLocallyUniformlyOn.inv₀_of_disjoint` `nhdsWithin_univ`

TendstoLocallyUniformlyOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`div₀` 📖	mathematical	`TendstoLocallyUniformlyOn` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `ContinuousOn` `UniformSpace.toTopologicalSpace`	`Pi.instDiv` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `NormedDivisionRing.toDivisionRing`	—	`div_eq_mul_inv` `mul₀` `NormSMulClass.toIsBoundedSMul` `NormMulClass.toNormSMulClass` `NormedDivisionRing.toNormMulClass` `inv₀` `ContinuousOn.inv₀` `NormedDivisionRing.to_continuousInv₀`
`fun_div₀` 📖	mathematical	`TendstoLocallyUniformlyOn` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `ContinuousOn` `UniformSpace.toTopologicalSpace`	`DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `NormedDivisionRing.toDivisionRing`	—	`div₀`
`fun_inv₀` 📖	mathematical	`TendstoLocallyUniformlyOn` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `ContinuousOn` `UniformSpace.toTopologicalSpace`	`InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid` `DivisionSemiring.toGroupWithZero` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing`	—	`inv₀`
`fun_inv₀_of_disjoint` 📖	mathematical	`TendstoLocallyUniformlyOn` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `Disjoint` `Filter` `Filter.instPartialOrder` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteLattice.toBoundedOrder` `Filter.instCompleteLatticeFilter` `Filter.map` `nhdsWithin` `nhds` `UniformSpace.toTopologicalSpace` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing`	`InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid` `DivisionSemiring.toGroupWithZero` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing`	—	`inv₀_of_disjoint`
`inv₀` 📖	mathematical	`TendstoLocallyUniformlyOn` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `ContinuousOn` `UniformSpace.toTopologicalSpace`	`Pi.instInv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid` `DivisionSemiring.toGroupWithZero` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing`	—	`inv₀_of_disjoint` `Disjoint.mono_left` `disjoint_nhds_nhds` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace`
`inv₀_of_disjoint` 📖	mathematical	`TendstoLocallyUniformlyOn` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `Disjoint` `Filter` `Filter.instPartialOrder` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteLattice.toBoundedOrder` `Filter.instCompleteLatticeFilter` `Filter.map` `nhdsWithin` `nhds` `UniformSpace.toTopologicalSpace` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing`	`Pi.instInv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid` `DivisionSemiring.toGroupWithZero` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing`	—	`tendstoLocallyUniformlyOn_iff_forall_tendsto` `Filter.HasBasis.disjoint_iff` `Filter.HasBasis.map` `Filter.basis_sets` `Metric.nhds_basis_ball` `Filter.Tendsto.comp` `Nat.instAtLeastTwoHAddOfNat` `uniformContinuousOn_inv₀` `compl_compl` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Real.instIsOrderedRing` `Real.instNontrivial` `Filter.tendsto_inf` `Filter.tendsto_principal` `Filter.mp_mem` `Filter.tendsto_snd` `Metric.dist_mem_uniformity` `half_pos` `Filter.univ_mem'` `dist_zero_right` `lt_of_not_ge` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.sub_congr` `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_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `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` `Nat.cast_one` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.add_pf_add_gt` `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.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Mathlib.Tactic.Linarith.add_lt_of_le_of_neg` `Mathlib.Tactic.Linarith.mul_nonpos` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Mathlib.Meta.NormNum.isNat_lt_true` `IsStrictOrderedRing.toCharZero` `CancelDenoms.sub_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_neg` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `dist_eq_norm_sub` `norm_sub_norm_le` `LT.lt.trans_le` `half_lt_self`

UniformContinuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fun_inv₀` 📖	mathematical	`UniformContinuous` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `Set` `Filter` `Filter.instMembership` `nhds` `UniformSpace.toTopologicalSpace` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `Compl.compl` `Set.instCompl` `Set.range`	`InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid` `DivisionSemiring.toGroupWithZero` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing`	—	`inv₀`
`inv₀` 📖	mathematical	`UniformContinuous` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `Set` `Filter` `Filter.instMembership` `nhds` `UniformSpace.toTopologicalSpace` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `Compl.compl` `Set.instCompl` `Set.range`	`Pi.instInv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid` `DivisionSemiring.toGroupWithZero` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing`	—	`UniformContinuousOn.inv₀`

UniformContinuousOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fun_inv₀` 📖	mathematical	`UniformContinuousOn` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `Set` `Filter` `Filter.instMembership` `nhds` `UniformSpace.toTopologicalSpace` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `Compl.compl` `Set.instCompl` `Set.image`	`InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid` `DivisionSemiring.toGroupWithZero` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing`	—	`inv₀`
`inv₀` 📖	mathematical	`UniformContinuousOn` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `Set` `Filter` `Filter.instMembership` `nhds` `UniformSpace.toTopologicalSpace` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `Compl.compl` `Set.instCompl` `Set.image`	`Pi.instInv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid` `DivisionSemiring.toGroupWithZero` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing`	—	`comp` `uniformContinuousOn_inv₀` `Set.mapsTo_image`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`tendsto_norm_inv_nhdsNE_zero_atTop` 📖	mathematical	—	`Filter.Tendsto` `Real` `Norm.norm` `NormedDivisionRing.toNorm` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid` `DivisionSemiring.toGroupWithZero` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet` `Filter.atTop` `Real.instPreorder`	—	`Filter.Tendsto.comp` `tendsto_norm_cobounded_atTop` `Filter.tendsto_inv₀_nhdsNE_zero`
`tendsto_zpow_nhdsNE_zero_cobounded` 📖	mathematical	—	`Filter.Tendsto` `DivInvMonoid.toZPow` `DivisionRing.toDivInvMonoid` `NormedDivisionRing.toDivisionRing` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet` `Bornology.cobounded` `PseudoMetricSpace.toBornology`	—	`neg_surjective` `CanLift.prf` `instCanLiftIntNatCastLeOfNat` `zpow_neg` `zpow_natCast` `inv_pow` `Filter.Tendsto.comp` `tendsto_pow_cobounded_cobounded` `NormedDivisionRing.to_normOneClass` `NormedDivisionRing.toNormMulClass` `Filter.tendsto_inv₀_nhdsNE_zero`
`uniformContinuousOn_inv₀` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `Compl.compl` `Set.instCompl`	`UniformContinuousOn` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid` `DivisionSemiring.toGroupWithZero` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing`	—	`Metric.uniformContinuousOn_iff_le` `Filter.HasBasis.mem_iff` `NormedAddCommGroup.nhds_zero_basis_norm_lt` `norm_pos_iff` `LT.lt.trans_le` `Set.subset_compl_comm` `mul_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `pow_pos` `IsStrictOrderedRing.toZeroLEOneClass` `dist_eq_norm` `inv_sub_inv'` `norm_mul` `NormedDivisionRing.toNormMulClass` `norm_inv` `dist_comm` `mul_le_mul` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `IsOrderedRing.toMulPosMono` `inv_anti₀` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `dist_nonneg` `le_of_lt` `inv_pos_of_pos` `inv_nonneg_of_nonneg` `norm_nonneg` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.inv_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.pow_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁` `one_mul` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero` `Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero` `ne_of_gt` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `div_one` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial`

---

← Back to Index