Documentation Verification Report

Units

📁 Source: Mathlib/Analysis/Normed/Ring/Units.lean

Statistics

Metric	Count
Definitions `add`, `ofNearby`	2
Theorems `closure_eq`, `isClosed`, `closure_ne_top`, `eq_top_of_norm_lt_one`, `inverse_add`, `inverse_add_norm`, `inverse_add_norm_diff_first_order`, `inverse_add_norm_diff_nth_order`, `inverse_add_norm_diff_second_order`, `inverse_add_nth_order`, `inverse_continuousAt`, `inverse_one_sub`, `inverse_one_sub_norm`, `inverse_one_sub_nth_order`, `inverse_one_sub_nth_order'`, `isOpen`, `isOpenEmbedding_val`, `isOpenMap_val`, `nhds`, `val_add`, `val_ofNearby`, `isClosed`, `subset_compl_ball`	23
Total	25

Ideal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`closure_ne_top` 📖	—	—	—	—	`closure_minimal` `coe_subset_nonunits` `nonunits.isClosed` `NonUnitalSeminormedRing.toIsTopologicalRing` `eq_top_iff_one` `one_notMem_nonunits`
`eq_top_of_norm_lt_one` 📖	mathematical	`Ideal` `Ring.toSemiring` `NormedRing.toRing` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Real` `Real.instLT` `Norm.norm` `NormedRing.toNorm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Real.instOne`	`Top.top` `Submodule.instTop`	—	`eq_top_iff_one` `sub_sub_cancel` `mul_mem_left`

Ideal.IsMaximal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`closure_eq` 📖	mathematical	—	`Ideal.closure` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedRing.toRing` `NonUnitalSeminormedRing.toIsTopologicalRing` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NormedRing.toNonUnitalNormedRing`	—	`NonUnitalSeminormedRing.toIsTopologicalRing` `eq_of_le` `Ideal.closure_ne_top` `ne_top` `subset_closure`
`isClosed` 📖	mathematical	—	`IsClosed` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `SetLike.coe` `Ideal` `Ring.toSemiring` `NormedRing.toRing` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`isClosed_of_closure_subset` `Eq.subset` `Set.instReflSubset` `NonUnitalSeminormedRing.toIsTopologicalRing` `closure_eq`

NormedRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`inverse_add` 📖	mathematical	—	`Filter.Eventually` `Ring.inverse` `Semiring.toMonoidWithZero` `Ring.toSemiring` `toRing` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Units.val` `MonoidWithZero.toMonoid` `Distrib.toMul` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Units` `Units.instInv` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `toSeminormedRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `nhds_discrete` `Finite.instDiscreteTopology` `T2Space.t1Space` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `Finite.of_subsingleton` `Metric.eventually_nhds_iff` `CancelDenoms.cancel_factors_lt` `Real.instIsStrictOrderedRing` `Mathlib.Meta.NormNum.isNat_lt_true` `Real.instIsOrderedRing` `IsStrictOrderedRing.toCharZero` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_zero` `Nat.cast_one` `Mathlib.Meta.NormNum.IsNat.to_eq` `Mathlib.Meta.NormNum.isNat_mul` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `one_mul` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `dist_zero_right` `Units.val_add` `Ring.inverse_unit` `Units.add.eq_1` `Units.copy_eq` `mul_inv_rev` `Units.val_mul` `Units.val_oneSub` `sub_neg_eq_add`
`inverse_add_norm` 📖	mathematical	—	`Asymptotics.IsBigO` `Real` `toNorm` `Real.norm` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `toSeminormedRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `toRing` `Ring.inverse` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Units.val` `MonoidWithZero.toMonoid` `Real.instOne`	—	`Filter.EventuallyEq.trans_isBigO` `inverse_add` `Continuous.tendsto'` `mulLeft_continuous` `NonUnitalSeminormedRing.toIsTopologicalRing` `MulZeroClass.mul_zero` `Asymptotics.IsBigO.mul` `NormedDivisionRing.toNormMulClass` `Asymptotics.IsBigO.comp_tendsto` `inverse_one_sub_norm` `Asymptotics.isBigO_const_const` `one_ne_zero` `NeZero.one` `Real.instNontrivial` `one_mul`
`inverse_add_norm_diff_first_order` 📖	mathematical	—	`Asymptotics.IsBigO` `Real` `toNorm` `Real.norm` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `toSeminormedRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `toRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `toNonUnitalNormedRing` `Ring.inverse` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Units.val` `MonoidWithZero.toMonoid` `Units` `Units.instInv` `Norm.norm`	—	`Finset.sum_congr` `neg_mul` `Finset.sum_singleton` `pow_zero` `one_mul` `pow_one` `inverse_add_norm_diff_nth_order`
`inverse_add_norm_diff_nth_order` 📖	mathematical	—	`Asymptotics.IsBigO` `Real` `toNorm` `Real.norm` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `toSeminormedRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `toRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `toNonUnitalNormedRing` `Ring.inverse` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Units.val` `MonoidWithZero.toMonoid` `Distrib.toMul` `Finset.sum` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Finset.range` `Monoid.toNatPow` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Units` `Units.instInv` `Real.instMonoid` `Norm.norm`	—	`Filter.EventuallyEq.trans_isBigO` `Filter.EventuallyEq.fun_sub` `inverse_add_nth_order` `Filter.EventuallyEq.refl` `add_sub_cancel_left` `Asymptotics.IsBigO.trans` `Asymptotics.IsBigO.mul` `NormedDivisionRing.toNormMulClass` `Asymptotics.IsBigO.norm_right` `Asymptotics.isBigO_refl` `inverse_add_norm` `mul_one` `Asymptotics.IsBigO.pow` `NormedDivisionRing.to_normOneClass` `Asymptotics.IsBigO.const_mul_left`
`inverse_add_norm_diff_second_order` 📖	mathematical	—	`Asymptotics.IsBigO` `Real` `toNorm` `Real.norm` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `toSeminormedRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `toRing` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `toNonUnitalNormedRing` `Ring.inverse` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Units.val` `MonoidWithZero.toMonoid` `Units` `Units.instInv` `Distrib.toMul` `Monoid.toNatPow` `Real.instMonoid` `Norm.norm`	—	`Finset.sum_congr` `neg_mul` `Finset.sum_range_succ` `Finset.sum_range_zero` `pow_zero` `zero_add` `pow_one` `add_mul` `Distrib.rightDistribClass` `one_mul` `sub_neg_eq_add` `inverse_add_norm_diff_nth_order`
`inverse_add_nth_order` 📖	mathematical	—	`Filter.Eventually` `Ring.inverse` `Semiring.toMonoidWithZero` `Ring.toSemiring` `toRing` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Units.val` `MonoidWithZero.toMonoid` `Distrib.toMul` `Finset.sum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `toSeminormedRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `toNonUnitalNormedRing` `Finset.range` `Monoid.toNatPow` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Units` `Units.instInv` `nhds` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`Continuous.tendsto'` `mulLeft_continuous` `NonUnitalSeminormedRing.toIsTopologicalRing` `MulZeroClass.mul_zero` `Filter.mp_mem` `Filter.Tendsto.eventually` `inverse_one_sub_nth_order` `inverse_add` `Filter.univ_mem'` `sub_neg_eq_add` `neg_mul` `add_mul` `Distrib.rightDistribClass` `mul_assoc`
`inverse_continuousAt` 📖	mathematical	—	`ContinuousAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `toSeminormedRing` `Ring.inverse` `Semiring.toMonoidWithZero` `Ring.toSemiring` `toRing` `Units.val` `MonoidWithZero.toMonoid`	—	`Asymptotics.IsBigO.trans_isLittleO` `inverse_add_norm_diff_first_order` `Asymptotics.IsLittleO.norm_left` `Asymptotics.isLittleO_id_const` `one_ne_zero` `NeZero.one` `Real.instNontrivial` `tendsto_zero_iff_norm_tendsto_zero` `tendsto_iff_norm_sub_tendsto_zero` `Filter.tendsto_id` `ContinuousAt.eq_1` `Ring.inverse_unit` `div_one` `add_sub_cancel` `Filter.Tendsto.comp` `Asymptotics.IsLittleO.tendsto_div_nhds_zero`
`inverse_one_sub` 📖	mathematical	`Real` `Real.instLT` `Norm.norm` `toNorm` `Real.instOne`	`Ring.inverse` `Semiring.toMonoidWithZero` `Ring.toSemiring` `toRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `toNonUnitalNormedRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Units.val` `MonoidWithZero.toMonoid` `Units` `Units.instInv` `Units.oneSub`	—	`Ring.inverse_unit` `Units.val_oneSub`
`inverse_one_sub_norm` 📖	mathematical	—	`Asymptotics.IsBigO` `Real` `toNorm` `Real.norm` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `toSeminormedRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `toRing` `Ring.inverse` `Semiring.toMonoidWithZero` `Ring.toSemiring` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `toNonUnitalNormedRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Real.instOne`	—	`Asymptotics.IsBigO_def` `Asymptotics.IsBigOWith_def` `Nat.instAtLeastTwoHAddOfNat` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Real.instIsOrderedRing` `Real.instNontrivial` `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.neg_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Tactic.Ring.neg_add` `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.sub_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `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.one_mul` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `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_neg` `neg_neg_of_pos` `Real.instIsOrderedAddMonoid` `Mathlib.Tactic.Linarith.zero_lt_one` `CancelDenoms.derive_trans` `Mathlib.Meta.NormNum.IsNNRat.to_eq` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `IsStrictOrderedRing.toCharZero` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.isNNRat_mul` `CancelDenoms.sub_subst` `CancelDenoms.div_subst` `Mathlib.Meta.NormNum.isNat_eq_true` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNat_mul` `Mathlib.Tactic.Linarith.mul_neg` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `dist_zero_right` `Mathlib.Meta.NormNum.isNat_lt_true` `Mathlib.Tactic.Linarith.mul_nonpos` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `inverse_one_sub` `NormOneClass.norm_one` `NormedDivisionRing.to_normOneClass` `mul_one` `tsum_geometric_le_of_norm_lt_one` `inv_le_of_inv_le₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `le_of_not_gt` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Tactic.Ring.inv_congr` `Mathlib.Tactic.Ring.atom_pf'` `Mathlib.Tactic.Linarith.add_lt_of_le_of_neg` `Mathlib.Tactic.Linarith.add_nonpos` `Mathlib.Tactic.Linarith.without_one_mul` `CancelDenoms.add_subst`
`inverse_one_sub_nth_order` 📖	mathematical	—	`Filter.Eventually` `Ring.inverse` `Semiring.toMonoidWithZero` `Ring.toSemiring` `toRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `toNonUnitalNormedRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Finset.sum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `toSeminormedRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Finset.range` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Distrib.toMul` `nhds` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`Metric.eventually_nhds_iff` `one_pos` `Real.instZeroLEOneClass` `NeZero.one` `Real.instNontrivial` `inverse_one_sub_nth_order'` `dist_zero_right`
`inverse_one_sub_nth_order'` 📖	mathematical	`Real` `Real.instLT` `Norm.norm` `toNorm` `Real.instOne`	`Ring.inverse` `Semiring.toMonoidWithZero` `Ring.toSemiring` `toRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `toNonUnitalNormedRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Finset.sum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `toSeminormedRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Finset.range` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Distrib.toMul`	—	`summable_geometric_of_norm_lt_one` `inverse_one_sub` `Summable.sum_add_tsum_nat_add` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `add_comm` `pow_add` `Summable.tsum_mul_left` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalSeminormedRing.toIsTopologicalRing` `SummationFilter.instNeBotUnconditional`

Units

Definitions

Name	Category	Theorems
`add` 📖	CompOp	1 math math: `val_add`
`ofNearby` 📖	CompOp	1 math math: `val_ofNearby`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isOpen` 📖	mathematical	—	`IsOpen` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `setOf` `IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NormedRing.toRing`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `Unique.instSubsingleton` `Finite.instDiscreteTopology` `T2Space.t1Space` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `Finite.of_subsingleton` `Metric.isOpen_iff` `inv_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `norm_pos` `isUnit` `mem_ball_iff_norm`
`isOpenEmbedding_val` 📖	mathematical	—	`Topology.IsOpenEmbedding` `Units` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NormedRing.toRing` `instTopologicalSpaceUnits` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `val`	—	`isEmbedding_val_mk'` `ContinuousAt.continuousWithinAt` `NormedRing.inverse_continuousAt` `Ring.inverse_unit` `isOpen`
`isOpenMap_val` 📖	mathematical	—	`IsOpenMap` `Units` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NormedRing.toRing` `instTopologicalSpaceUnits` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `val`	—	`Topology.IsOpenEmbedding.isOpenMap` `isOpenEmbedding_val`
`nhds` 📖	mathematical	—	`Set` `Filter` `Filter.instMembership` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `val` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NormedRing.toRing` `setOf` `IsUnit`	—	`IsOpen.mem_nhds` `isOpen` `isUnit`
`val_add` 📖	mathematical	`Real` `Real.instLT` `Norm.norm` `NormedRing.toNorm` `Real.instInv` `val` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NormedRing.toRing` `Units` `instInv`	`add` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	—
`val_ofNearby` 📖	mathematical	`Real` `Real.instLT` `Norm.norm` `NormedRing.toNorm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing` `val` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NormedRing.toRing` `Real.instInv` `Units` `instInv`	`ofNearby`	—	—

nonunits

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isClosed` 📖	mathematical	—	`IsClosed` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `nonunits` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NormedRing.toRing`	—	`IsOpen.isClosed_compl` `Units.isOpen`
`subset_compl_ball` 📖	mathematical	—	`Set` `Set.instHasSubset` `nonunits` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NormedRing.toRing` `Compl.compl` `Set.instCompl` `Metric.ball` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Real` `Real.instOne`	—	`Units.isUnit` `mem_ball_iff_norm'` `sub_sub_self`

---

← Back to Index