ControlledClosure

📁 Source: Mathlib/Analysis/Normed/Group/ControlledClosure.lean

Statistics

Metric	Count
Definitions	0
Theorems controlled_closure_of_complete, controlled_closure_range_of_complete	2
Total	2

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
controlled_closure_of_complete 📖	mathematical	Real Real.instLT Real.instZero NormedAddGroupHom.SurjectiveOnWith NormedAddCommGroup.toSeminormedAddCommGroup	AddSubgroup.topologicalClosure UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup Real.instAdd	—	SeminormedAddCommGroup.toIsTopologicalAddGroup map_zero AddMonoidHomClass.toZeroHomClass NormedAddGroupHom.toAddMonoidHomClass norm_zero MulZeroClass.mul_zero Nat.instAtLeastTwoHAddOfNat div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing mul_pos pow_pos IsStrictOrderedRing.toZeroLEOneClass Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Meta.NormNum.instAtLeastTwo norm_pos_iff controlled_sum_of_mem_closure NormedAddCommGroup.cauchy_series_of_le_geometric'' one_div one_half_lt_one mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono LT.lt.le le_of_lt inv_pow mul_div_cancel₀ LT.lt.ne mul_comm cauchySeq_tendsto_of_complete map_sum Finset.sum_congr tendsto_nhds_unique TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat Filter.Tendsto.comp Continuous.tendsto NormedAddGroupHom.continuous norm_le_insert' add_le_add_right IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid add_comm mul_add Distrib.leftDistribClass mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono sum_geometric_two_le two_ne_zero CharZero.NeZero.two IsStrictOrderedRing.toCharZero norm_sum_le Finset.sum_range_succ' add_le_add_left covariant_swap_add_of_covariant_add Finset.sum_le_sum add_le_add add_assoc add_mul Distrib.rightDistribClass le_of_tendsto' instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal ContinuousAt.tendsto Continuous.continuousAt continuous_norm
controlled_closure_range_of_complete 📖	mathematical	Norm.norm NormedAddCommGroup.toNorm DFunLike.coe NormedAddGroupHom NormedAddCommGroup.toSeminormedAddCommGroup NormedAddGroupHom.funLike SeminormedAddCommGroup.toNorm Real Real.instLT Real.instZero Real.instLE Real.instMul	NormedAddGroupHom.SurjectiveOnWith AddSubgroup.topologicalClosure UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup NormedAddGroupHom.range Real.instAdd	—	NormedAddGroupHom.mem_range controlled_closure_of_complete

---

← Back to Index