Uniformizable

📁 Source: Mathlib/Topology/UniformSpace/Uniformizable.lean

Statistics

Metric	Count
Definitions	0
Theorems exists_uniformSpace, of_exists_uniformSpace, toCompletelyRegularSpace, completelyRegularSpace_iff_exists_uniformSpace	4
Total	4

CompletelyRegularSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_uniformSpace 📖	mathematical	—	UniformSpace.toTopologicalSpace	—	TopologicalSpace.isOpen_univ instCompactSpaceStoneCech T2Space.r1Space instT2SpaceStoneCech Topology.IsInducing.eq_induced isInducing_stoneCechUnit
of_exists_uniformSpace 📖	mathematical	UniformSpace.toTopologicalSpace	CompletelyRegularSpace	—	UniformSpace.toCompletelyRegularSpace

UniformSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toCompletelyRegularSpace 📖	mathematical	—	CompletelyRegularSpace toTopologicalSpace	—	Real.instIsOrderedRing isOpen_iff_isOpen_ball_subset IsClosed.isOpen_compl comp_comp_symm_mem_uniformity_sets HasSubset.Subset.trans Set.instIsTransSubset SetRel.comp_subset_comp_left SetRel.comp_subset_comp_right interior_subset isOpen_interior interior_mem_uniformity ball_mono isClosed_closure isOpen_ball closure_ball_subset closure_eq_inter_uniformity Set.iInter_congr_Prop Set.iInter₂_subset Urysohns.CU.lim_mem_Icc Urysohns.CU.continuous_lim Urysohns.CU.lim_of_mem_C subset_closure refl_mem_uniformity Urysohns.CU.lim_of_notMem_U

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
completelyRegularSpace_iff_exists_uniformSpace 📖	mathematical	—	CompletelyRegularSpace UniformSpace.toTopologicalSpace	—	CompletelyRegularSpace.exists_uniformSpace CompletelyRegularSpace.of_exists_uniformSpace

---

← Back to Index