Urysohn

📁 Source: Mathlib/Topology/Metrizable/Urysohn.lean

Statistics

Metric	Count
Definitions	0
Theorems of_regularSpace_secondCountableTopology, exists_embedding_l_infty, exists_isInducing_l_infty, metrizableSpace_of_t3_secondCountable	4
Total	4

TopologicalSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_embedding_l_infty 📖	mathematical	—	Topology.IsEmbedding BoundedContinuousFunction Real instTopologicalSpaceNat Real.pseudoMetricSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace BoundedContinuousFunction.instPseudoMetricSpace	—	exists_isInducing_l_infty T3Space.toRegularSpace Topology.IsInducing.isEmbedding T3Space.toT0Space
exists_isInducing_l_infty 📖	mathematical	—	Topology.IsInducing BoundedContinuousFunction Real instTopologicalSpaceNat Real.pseudoMetricSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace BoundedContinuousFunction.instPseudoMetricSpace	—	exists_countable_basis Disjoint.mono_right Set.compl_subset_compl disjoint_compl_right zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing Set.Countable.mono Set.inter_subset_left Set.Countable.prod LE.le.trans le_hasSum Real.instIsOrderedAddMonoid OrderTopology.to_orderClosedTopology instOrderTopologyReal SummationFilter.instNeBotUnconditional SummationFilter.instLeAtTopUnconditional LT.lt.le Summable.tendsto_cofinite_zero instIsTopologicalAddGroupReal HasSum.summable exists_continuous_zero_one_of_isClosed CompletelyNormalSpace.toNormalSpace CompletelyNormalSpace.of_regularSpace_secondCountableTopology isClosed_closure IsOpen.isClosed_compl IsTopologicalBasis.isOpen UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal subset_closure MulZeroClass.mul_zero mul_one mul_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing mul_le_of_le_one_right Set.Icc_subset_Icc_right continuous_of_discreteTopology Real.dist_le_of_mem_Icc_01 Topology.isInducing_iff_nhds le_antisymm Filter.HasBasis.ge_iff Filter.HasBasis.comap Metric.nhds_basis_closedBall gt_mem_nhds Filter.eventually_all_finite Continuous.tendsto ContinuousMap.continuous Metric.closedBall_mem_nhds Filter.Eventually.mono BoundedContinuousFunction.dist_le le_total Real.dist_le_of_mem_Icc sub_zero Filter.HasBasis.le_basis_iff Metric.nhds_basis_ball IsTopologicalBasis.nhds_hasBasis IsTopologicalBasis.exists_closure_subset IsTopologicalBasis.mem_nhds LE.le.trans_lt BoundedContinuousFunction.dist_coe_le_dist Mathlib.Tactic.Contrapose.contrapose₁ Pi.zero_apply dist_zero_right le_abs_self instDiscreteTopologyNat Topology.IsInducing.comp Topology.IsEmbedding.isInducing Isometry.isEmbedding BoundedContinuousFunction.isometry_extend
metrizableSpace_of_t3_secondCountable 📖	mathematical	—	MetrizableSpace	—	exists_embedding_l_infty Topology.IsEmbedding.metrizableSpace EMetricSpace.metrizableSpace

TopologicalSpace.PseudoMetrizableSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_regularSpace_secondCountableTopology 📖	mathematical	—	TopologicalSpace.PseudoMetrizableSpace	—	TopologicalSpace.exists_isInducing_l_infty Topology.IsInducing.pseudoMetrizableSpace PseudoEMetricSpace.pseudoMetrizableSpace

---

← Back to Index