ShrinkingLemma

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

Statistics

Metric	Count
Definitions	0
Theorems exists_iUnion_ball_eq_radius_lt, exists_iUnion_ball_eq_radius_pos_lt, exists_locallyFinite_iUnion_eq_ball_radius_lt, exists_locallyFinite_subset_iUnion_ball_radius_lt, exists_subset_iUnion_ball_radius_lt, exists_subset_iUnion_ball_radius_pos_lt	6
Total	6

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_iUnion_ball_eq_radius_lt 📖	mathematical	Set.Finite setOf Set Set.instMembership Metric.ball MetricSpace.toPseudoMetricSpace Set.iUnion Set.univ	Real Real.instLT	—	exists_subset_iUnion_ball_radius_lt isClosed_univ Eq.ge Set.univ_subset_iff
exists_iUnion_ball_eq_radius_pos_lt 📖	mathematical	Real Real.instLT Real.instZero Set.Finite setOf Set Set.instMembership Metric.ball MetricSpace.toPseudoMetricSpace Set.iUnion Set.univ	Set.Ioo Real.instPreorder	—	exists_subset_iUnion_ball_radius_pos_lt isClosed_univ Eq.ge Set.univ_subset_iff
exists_locallyFinite_iUnion_eq_ball_radius_lt 📖	mathematical	Real Real.instLT Real.instZero	LocallyFinite UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace Metric.ball Set.iUnion Set.univ	—	exists_locallyFinite_subset_iUnion_ball_radius_lt isClosed_univ Set.univ_subset_iff
exists_locallyFinite_subset_iUnion_ball_radius_lt 📖	mathematical	Real Real.instLT Real.instZero	Set Set.instMembership LocallyFinite UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace Metric.ball Set.instHasSubset Set.iUnion	—	nhds_basis_uniformity Metric.uniformity_basis_dist_lt refinement_of_locallyCompact_sigmaCompact_of_nhds_basis_set instWeaklyLocallyCompactSpaceOfLocallyCompactSpace locallyCompact_of_proper sigmaCompactSpace_of_locallyCompact_secondCountable secondCountable_of_proper TopologicalSpace.t2Space_of_metrizableSpace TopologicalSpace.PseudoMetrizableSpace.toMetrizableSpace MetricSpace.instT0Space UniformSpace.pseudoMetrizableSpace EMetric.instIsCountablyGeneratedUniformity exists_subset_iUnion_ball_radius_pos_lt LocallyFinite.point_finite
exists_subset_iUnion_ball_radius_lt 📖	mathematical	Set.Finite setOf Set Set.instMembership Metric.ball MetricSpace.toPseudoMetricSpace Set.instHasSubset Set.iUnion	Real Real.instLT	—	exists_subset_iUnion_closed_subset T4Space.toNormalSpace T4Space.of_paracompactSpace_t2Space TopologicalSpace.t2Space_of_metrizableSpace TopologicalSpace.PseudoMetrizableSpace.toMetrizableSpace MetricSpace.instT0Space UniformSpace.pseudoMetrizableSpace EMetric.instIsCountablyGeneratedUniformity Metric.instParacompactSpace Metric.isOpen_ball exists_lt_subset_ball HasSubset.Subset.trans Set.instIsTransSubset Set.iUnion_mono
exists_subset_iUnion_ball_radius_pos_lt 📖	mathematical	Real Real.instLT Real.instZero Set.Finite setOf Set Set.instMembership Metric.ball MetricSpace.toPseudoMetricSpace Set.instHasSubset Set.iUnion	Set.Ioo Real.instPreorder	—	exists_subset_iUnion_closed_subset T4Space.toNormalSpace T4Space.of_paracompactSpace_t2Space TopologicalSpace.t2Space_of_metrizableSpace TopologicalSpace.PseudoMetrizableSpace.toMetrizableSpace MetricSpace.instT0Space UniformSpace.pseudoMetrizableSpace EMetric.instIsCountablyGeneratedUniformity Metric.instParacompactSpace Metric.isOpen_ball exists_pos_lt_subset_ball HasSubset.Subset.trans Set.instIsTransSubset Set.iUnion_mono

---

← Back to Index