Lemmas

📁 Source: Mathlib/Topology/MetricSpace/Pseudo/Lemmas.lean

Statistics

Metric	Count
Definitions	0
Theorems biInter_gt_ball, biInter_gt_closedBall, biUnion_lt_ball, biUnion_lt_closedBall, closedBall_zero', closure_ball_subset_closedBall, closure_closedBall, closure_sphere, eventually_isCompact_closedBall, exists_isCompact_closedBall, frontier_ball_subset_sphere, frontier_closedBall_subset_sphere, isClosed_closedBall, isClosed_sphere, singleton_eq_inter_Icc, eventually_ball_subset, eventually_closedBall_subset, instOrderTopologyReal, lebesgue_number_lemma_of_metric, lebesgue_number_lemma_of_metric_sUnion, squeeze_zero, squeeze_zero', tendsto_closedBall_smallSets	23
Total	23

Metric

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
biInter_gt_ball 📖	mathematical	—	Set.iInter Real Real.instLT ball closedBall	—	Set.ext Set.iInter_congr_Prop
biInter_gt_closedBall 📖	mathematical	—	Set.iInter Real Real.instLT closedBall	—	Set.ext Set.iInter_congr_Prop LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing
biUnion_lt_ball 📖	mathematical	—	Set.iUnion Real Real.instLT ball	—	Set.ext not_iff_not LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing
biUnion_lt_closedBall 📖	mathematical	—	Set.iUnion Real Real.instLT closedBall ball	—	Set.ext not_iff_not
closedBall_zero' 📖	mathematical	—	closedBall Real Real.instZero closure UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Set Set.instSingletonSet	—	Set.Subset.antisymm mem_closure_iff Set.mem_singleton LE.le.trans_lt mem_closedBall closure_minimal Set.singleton_subset_iff Eq.le dist_self isClosed_closedBall
closure_ball_subset_closedBall 📖	mathematical	—	Set Set.instHasSubset closure UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace ball closedBall	—	closure_minimal ball_subset_closedBall isClosed_closedBall
closure_closedBall 📖	mathematical	—	closure UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace closedBall	—	IsClosed.closure_eq isClosed_closedBall
closure_sphere 📖	mathematical	—	closure UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace sphere	—	IsClosed.closure_eq isClosed_sphere
eventually_isCompact_closedBall 📖	mathematical	—	Filter.Eventually Real IsCompact UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace closedBall nhds Real.pseudoMetricSpace Real.instZero	—	WeaklyLocallyCompactSpace.exists_compact_mem_nhds Filter.mp_mem eventually_closedBall_subset Filter.univ_mem' IsCompact.of_isClosed_subset isClosed_closedBall
exists_isCompact_closedBall 📖	mathematical	—	Real Real.instLT Real.instZero IsCompact UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace closedBall	—	eventually_nhdsWithin_of_eventually_nhds eventually_isCompact_closedBall Filter.Eventually.exists nhdsGT_neBot instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial Filter.Eventually.and self_mem_nhdsWithin
frontier_ball_subset_sphere 📖	mathematical	—	Set Set.instHasSubset frontier UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace ball sphere	—	frontier_lt_subset_eq OrderTopology.to_orderClosedTopology instOrderTopologyReal Continuous.dist continuous_id' continuous_const
frontier_closedBall_subset_sphere 📖	mathematical	—	Set Set.instHasSubset frontier UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace closedBall sphere	—	frontier_le_subset_eq OrderTopology.to_orderClosedTopology instOrderTopologyReal Continuous.dist continuous_id' continuous_const
isClosed_closedBall 📖	mathematical	—	IsClosed UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace closedBall	—	isClosed_le OrderTopology.to_orderClosedTopology instOrderTopologyReal Continuous.dist continuous_id' continuous_const
isClosed_sphere 📖	mathematical	—	IsClosed UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace sphere	—	isClosed_eq OrderClosedTopology.to_t2Space OrderTopology.to_orderClosedTopology instOrderTopologyReal Continuous.dist continuous_id' continuous_const

Real

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
singleton_eq_inter_Icc 📖	mathematical	—	Real Set Set.instSingletonSet Set.iInter instLT instZero Set.Icc instPreorder instSub instAdd	—	Set.iInter_congr_Prop Nat.instAtLeastTwoHAddOfNat Icc_eq_closedBall sub_add_add_cancel add_self_div_two ZeroLEOneClass.neZero.two instZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero instIsStrictOrderedRing IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid add_sub_sub_cancel biInter_basis_nhds Metric.nhds_basis_closedBall T2Space.t1Space OrderClosedTopology.to_t2Space OrderTopology.to_orderClosedTopology instOrderTopologyReal

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eventually_ball_subset 📖	mathematical	Set Filter Filter.instMembership nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace	Filter.Eventually Real Set.instHasSubset Metric.ball Real.pseudoMetricSpace Real.instZero	—	Filter.Eventually.mono eventually_closedBall_subset HasSubset.Subset.trans Set.instIsTransSubset Metric.ball_subset_closedBall
eventually_closedBall_subset 📖	mathematical	Set Filter Filter.instMembership nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace	Filter.Eventually Real Set.instHasSubset Metric.closedBall Real.pseudoMetricSpace Real.instZero	—	Filter.HasBasis.mem_iff Metric.nhds_basis_closedBall Iic_mem_nhds instClosedIciTopology OrderTopology.to_orderClosedTopology instOrderTopologyReal Filter.mp_mem Filter.univ_mem' Set.Subset.trans Metric.closedBall_subset_closedBall
instOrderTopologyReal 📖	mathematical	—	OrderTopology Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instPreorder	—	orderTopology_of_nhds_abs Real.instIsOrderedAddMonoid Filter.HasBasis.eq_biInf Metric.nhds_basis_ball iInf_congr_Prop abs_sub_comm
lebesgue_number_lemma_of_metric 📖	mathematical	IsCompact UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace IsOpen Set Set.instHasSubset Set.iUnion	Real Real.instLT Real.instZero Metric.ball	—	dist_comm Filter.HasBasis.lebesgue_number_lemma Metric.uniformity_basis_dist
lebesgue_number_lemma_of_metric_sUnion 📖	mathematical	IsCompact UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace IsOpen Set Set.instHasSubset Set.sUnion	Real Real.instLT Real.instZero Set.instMembership Metric.ball	—	lebesgue_number_lemma_of_metric Set.sUnion_eq_iUnion
squeeze_zero 📖	—	Real Real.instLE Real.instZero Filter.Tendsto nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	—	—	squeeze_zero' Filter.Eventually.of_forall
squeeze_zero' 📖	—	Filter.Eventually Real Real.instLE Real.instZero Filter.Tendsto nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	—	—	tendsto_of_tendsto_of_tendsto_of_le_of_le' instOrderTopologyReal tendsto_const_nhds
tendsto_closedBall_smallSets 📖	mathematical	—	Filter.Tendsto Real Set Metric.closedBall nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instZero Filter.smallSets	—	Filter.tendsto_smallSets_iff eventually_closedBall_subset

---

← Back to Index