PartitionOfUnity

📁 Source: Mathlib/Topology/MetricSpace/PartitionOfUnity.lean

Statistics

Metric	Count
Definitions	0
Theorems eventually_nhds_zero_forall_closedBall_subset, exists_continuous_eNNReal_forall_closedBall_subset, exists_continuous_nnreal_forall_closedBall_subset, exists_continuous_real_forall_closedBall_subset, exists_forall_closedBall_subset_aux₁, exists_forall_closedBall_subset_aux₂, eventually_nhds_zero_forall_closedEBall_subset, exists_continuous_ennreal_forall_closedEBall_subset, exists_continuous_nnreal_forall_closedBall_subset, exists_continuous_nnreal_forall_closedEBall_subset, exists_continuous_real_forall_closedBall_subset, exists_continuous_real_forall_closedEBall_subset, exists_forall_closedEBall_subset_aux₁, exists_forall_closedEBall_subset_aux₂	14
Total	14

EMetric

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eventually_nhds_zero_forall_closedBall_subset 📖	mathematical	IsClosed UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace EMetricSpace.toPseudoEMetricSpace IsOpen Set Set.instHasSubset LocallyFinite	Filter.Eventually ENNReal SProd.sprod Filter Filter.instSProd nhds ENNReal.instTopologicalSpace instZeroENNReal	—	Metric.eventually_nhds_zero_forall_closedEBall_subset
exists_continuous_eNNReal_forall_closedBall_subset 📖	mathematical	IsClosed UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace EMetricSpace.toPseudoEMetricSpace IsOpen Set Set.instHasSubset LocallyFinite	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal DFunLike.coe ContinuousMap ENNReal.instTopologicalSpace ContinuousMap.instFunLike Metric.closedEBall	—	Metric.exists_continuous_ennreal_forall_closedEBall_subset
exists_continuous_nnreal_forall_closedBall_subset 📖	mathematical	IsClosed UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace EMetricSpace.toPseudoEMetricSpace IsOpen Set Set.instHasSubset LocallyFinite	NNReal Preorder.toLT PartialOrder.toPreorder instPartialOrderNNReal instZeroNNReal DFunLike.coe ContinuousMap NNReal.instTopologicalSpace ContinuousMap.instFunLike Metric.closedEBall ENNReal.ofNNReal	—	Metric.exists_continuous_nnreal_forall_closedEBall_subset
exists_continuous_real_forall_closedBall_subset 📖	mathematical	IsClosed UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace EMetricSpace.toPseudoEMetricSpace IsOpen Set Set.instHasSubset LocallyFinite	Real Real.instLT Real.instZero DFunLike.coe ContinuousMap PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.instFunLike Metric.closedEBall ENNReal.ofReal	—	Metric.exists_continuous_real_forall_closedEBall_subset
exists_forall_closedBall_subset_aux₁ 📖	mathematical	IsClosed UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace EMetricSpace.toPseudoEMetricSpace IsOpen Set Set.instHasSubset LocallyFinite	Filter.Eventually Real Set.instMembership Set.instInter Set.Ioi Real.instPreorder Real.instZero Set.preimage ENNReal ENNReal.ofReal Set.iInter setOf Metric.closedEBall nhds	—	Metric.exists_forall_closedEBall_subset_aux₁
exists_forall_closedBall_subset_aux₂ 📖	mathematical	—	Convex Real Real.semiring Real.partialOrder Real.instAddCommMonoid Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id Set Set.instInter Set.Ioi Real.instPreorder Real.instZero Set.preimage ENNReal ENNReal.ofReal Set.iInter Set.instMembership setOf Set.instHasSubset Metric.closedEBall EMetricSpace.toPseudoEMetricSpace	—	Metric.exists_forall_closedEBall_subset_aux₂

Metric

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eventually_nhds_zero_forall_closedEBall_subset 📖	mathematical	IsClosed UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace EMetricSpace.toPseudoEMetricSpace IsOpen Set Set.instHasSubset LocallyFinite	Filter.Eventually ENNReal SProd.sprod Filter Filter.instSProd nhds ENNReal.instTopologicalSpace instZeroENNReal	—	Filter.HasBasis.mem_iff nhds_basis_closedEBall IsOpen.mem_nhds ENNReal.lt_iff_exists_nnreal_btwn Filter.mp_mem Filter.prod_mem_prod eventually_lt_nhds instClosedIciTopology OrderTopology.to_orderClosedTopology ENNReal.instOrderTopology closedEBall_mem_nhds tsub_pos_iff_lt ENNReal.instCanonicallyOrderedAdd ENNReal.instOrderedSub Filter.univ_mem' PseudoEMetricSpace.edist_triangle add_le_add IsOrderedAddMonoid.toAddLeftMono ENNReal.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add le_trans tsub_le_tsub_left LT.lt.le Membership.mem.out add_tsub_cancel_of_le CanonicallyOrderedAdd.toExistsAddOfLE lt_trans Filter.eventually_all_finite LocallyFinite.point_finite Filter.tendsto_snd LocallyFinite.iInter_compl_mem_nhds
exists_continuous_ennreal_forall_closedEBall_subset 📖	mathematical	IsClosed UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace EMetricSpace.toPseudoEMetricSpace IsOpen Set Set.instHasSubset LocallyFinite	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal DFunLike.coe ContinuousMap ENNReal.instTopologicalSpace ContinuousMap.instFunLike closedEBall	—	exists_continuous_nnreal_forall_closedEBall_subset ENNReal.continuous_coe ENNReal.coe_pos
exists_continuous_nnreal_forall_closedBall_subset 📖	mathematical	IsClosed UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace IsOpen Set Set.instHasSubset LocallyFinite	NNReal Preorder.toLT PartialOrder.toPreorder instPartialOrderNNReal instZeroNNReal DFunLike.coe ContinuousMap NNReal.instTopologicalSpace ContinuousMap.instFunLike closedBall NNReal.toReal	—	exists_continuous_nnreal_forall_closedEBall_subset closedEBall_coe
exists_continuous_nnreal_forall_closedEBall_subset 📖	mathematical	IsClosed UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace EMetricSpace.toPseudoEMetricSpace IsOpen Set Set.instHasSubset LocallyFinite	NNReal Preorder.toLT PartialOrder.toPreorder instPartialOrderNNReal instZeroNNReal DFunLike.coe ContinuousMap NNReal.instTopologicalSpace ContinuousMap.instFunLike closedEBall ENNReal.ofNNReal	—	exists_continuous_real_forall_closedEBall_subset CanLift.prf NNReal.ContinuousMap.canLift LT.lt.le
exists_continuous_real_forall_closedBall_subset 📖	mathematical	IsClosed UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace IsOpen Set Set.instHasSubset LocallyFinite	Real Real.instLT Real.instZero DFunLike.coe ContinuousMap Real.pseudoMetricSpace ContinuousMap.instFunLike closedBall	—	exists_continuous_nnreal_forall_closedBall_subset NNReal.continuous_coe
exists_continuous_real_forall_closedEBall_subset 📖	mathematical	IsClosed UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace EMetricSpace.toPseudoEMetricSpace IsOpen Set Set.instHasSubset LocallyFinite	Real Real.instLT Real.instZero DFunLike.coe ContinuousMap PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.instFunLike closedEBall ENNReal.ofReal	—	forall_swap exists_continuous_forall_mem_convex_of_local_const T4Space.toNormalSpace T4Space.of_paracompactSpace_t2Space TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace instParacompactSpace IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul exists_forall_closedEBall_subset_aux₂ exists_forall_closedEBall_subset_aux₁
exists_forall_closedEBall_subset_aux₁ 📖	mathematical	IsClosed UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace EMetricSpace.toPseudoEMetricSpace IsOpen Set Set.instHasSubset LocallyFinite	Filter.Eventually Real Set.instMembership Set.instInter Set.Ioi Real.instPreorder Real.instZero Set.preimage ENNReal ENNReal.ofReal Set.iInter setOf closedEBall nhds	—	Filter.Tendsto.eventually Continuous.tendsto' ENNReal.continuous_ofReal ENNReal.ofReal_zero Filter.Eventually.curry eventually_nhds_zero_forall_closedEBall_subset Filter.Eventually.exists_gt nhdsGT_neBot instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial Filter.Eventually.mono Set.mem_preimage Set.mem_iInter₂
exists_forall_closedEBall_subset_aux₂ 📖	mathematical	—	Convex Real Real.semiring Real.partialOrder Real.instAddCommMonoid Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id Set Set.instInter Set.Ioi Real.instPreorder Real.instZero Set.preimage ENNReal ENNReal.ofReal Set.iInter Set.instMembership setOf Set.instHasSubset closedEBall EMetricSpace.toPseudoEMetricSpace	—	Convex.inter convex_Ioi Real.instIsOrderedCancelAddMonoid IsStrictOrderedModule.toPosSMulStrictMono IsStrictOrderedRing.toIsStrictOrderedModule Real.instIsStrictOrderedRing Set.OrdConnected.convex Real.instIsOrderedAddMonoid IsOrderedModule.toPosSMulMono IsStrictOrderedModule.toIsOrderedModule Set.OrdConnected.preimage_ennreal_ofReal Set.ordConnected_iInter ordConnected_setOf_closedEBall_subset

---

← Back to Index