Separation

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

Statistics

Metric	Count
Definitions instUniformSpace, lift', map	3
Theorems inseparable_iff_uniformity, specializes_iff_uniformity, inseparable_iff_uniformity, nhds_le_uniformity, comap_map_mk_uniformity, comap_mk_uniformity, lift'_mk, map_comp, map_id, map_mk, map_unique, uniformContinuous_dom, uniformContinuous_dom₂, uniformContinuous_lift, uniformContinuous_lift', uniformContinuous_map, uniformContinuous_mk, uniformContinuous_uncurry_lift₂, uniformity_eq, completelyNormalSpace_of_hasAntitoneBasis, completelyNormalSpace_of_isCountablyGenerated_uniformity, to_regularSpace, eq_of_clusterPt_uniformity, eq_of_forall_symmetric, eq_of_uniformity, eq_of_uniformity_basis, inseparable_iff_clusterPt_uniformity, inseparable_iff_ker_uniformity, isClosed_of_spaced_out, isClosed_range_of_spaced_out, t0Space_iff_ker_uniformity, t0Space_iff_uniformity, t0Space_iff_uniformity'	33
Total	36

Filter.HasBasis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inseparable_iff_uniformity 📖	mathematical	Filter.HasBasis uniformity	Inseparable UniformSpace.toTopologicalSpace Set Set.instMembership	—	specializes_iff_inseparable instR0Space instR1Space UniformSpace.to_regularSpace specializes_iff_uniformity
specializes_iff_uniformity 📖	mathematical	Filter.HasBasis uniformity	Specializes UniformSpace.toTopologicalSpace Set Set.instMembership	—	specializes_iff nhds_basis_uniformity

Filter.Tendsto

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inseparable_iff_uniformity 📖	mathematical	Filter.Tendsto nhds UniformSpace.toTopologicalSpace	Inseparable uniformity	—	mono_right prodMk_nhds Inseparable.nhds_le_uniformity inseparable_iff_clusterPt_uniformity ClusterPt.mono ClusterPt.of_le_nhds Filter.map_neBot

Inseparable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
nhds_le_uniformity 📖	mathematical	Inseparable UniformSpace.toTopologicalSpace	Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder nhds instTopologicalSpaceProd uniformity	—	prod rfl nhds_le_uniformity

SeparationQuotient

Definitions

Name	Category	Theorems
instUniformSpace 📖	CompOp	21 math math: uniformity_eq, uniformContinuous_mk, instIsUniformGroup, isUniformInducing_mk, outCLM_uniformContinuous, uniformContinuous_lift, uniformContinuous_lift', uniformContinuous_dom₂, outCLM_isUniformEmbedding, completeSpace_iff, instIsUniformAddGroup, uniformContinuous_uncurry_lift₂, IsUltraUniformity.separationQuotient_iff, IsUltraUniformity.separationQuotient, UniformSpace.Completion.uniformContinuous_completionSeparationQuotientEquiv_symm, comap_mk_uniformity, uniformContinuous_map, instCompleteSpace, UniformSpace.Completion.uniformContinuous_completionSeparationQuotientEquiv, uniformContinuous_dom, outCLM_isUniformInducing
lift' 📖	CompOp	2 math math: uniformContinuous_lift', lift'_mk
map 📖	CompOp	5 math math: map_id, uniformContinuous_map, map_comp, map_unique, map_mk

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comap_map_mk_uniformity 📖	mathematical	—	Filter.comap SeparationQuotient UniformSpace.toTopologicalSpace Filter.map uniformity	—	le_antisymm Filter.HasBasis.le_basis_iff Filter.HasBasis.comap Filter.HasBasis.map Filter.basis_sets uniformity_hasBasis_open Inseparable.mem_open_iff Inseparable.prod Filter.le_comap_map
comap_mk_uniformity 📖	mathematical	—	Filter.comap SeparationQuotient UniformSpace.toTopologicalSpace uniformity instUniformSpace	—	comap_map_mk_uniformity
lift'_mk 📖	mathematical	UniformContinuous	lift' UniformSpace.toTopologicalSpace	—	lift'.eq_1
map_comp 📖	mathematical	UniformContinuous	SeparationQuotient UniformSpace.toTopologicalSpace map	—	map_unique UniformContinuous.comp
map_id 📖	mathematical	—	map SeparationQuotient UniformSpace.toTopologicalSpace	—	map_unique uniformContinuous_id
map_mk 📖	mathematical	UniformContinuous	map UniformSpace.toTopologicalSpace	—	map.eq_1 instT0Space UniformContinuous.comp
map_unique 📖	mathematical	UniformContinuous SeparationQuotient UniformSpace.toTopologicalSpace	map	—	—
uniformContinuous_dom 📖	mathematical	—	UniformContinuous SeparationQuotient UniformSpace.toTopologicalSpace instUniformSpace	—	—
uniformContinuous_dom₂ 📖	mathematical	—	UniformContinuous SeparationQuotient UniformSpace.toTopologicalSpace instUniformSpaceProd instUniformSpace	—	uniformity_prod_eq_prod Filter.prod_map_map_eq
uniformContinuous_lift 📖	mathematical	—	UniformContinuous SeparationQuotient UniformSpace.toTopologicalSpace instUniformSpace lift	—	—
uniformContinuous_lift' 📖	mathematical	—	UniformContinuous SeparationQuotient UniformSpace.toTopologicalSpace instUniformSpace lift'	—	lift'.eq_1 uniformContinuous_lift uniformContinuous_of_const
uniformContinuous_map 📖	mathematical	—	UniformContinuous SeparationQuotient UniformSpace.toTopologicalSpace instUniformSpace map	—	uniformContinuous_lift'
uniformContinuous_mk 📖	mathematical	—	UniformContinuous SeparationQuotient UniformSpace.toTopologicalSpace instUniformSpace	—	le_rfl
uniformContinuous_uncurry_lift₂ 📖	mathematical	—	UniformContinuous SeparationQuotient UniformSpace.toTopologicalSpace instUniformSpaceProd instUniformSpace lift₂	—	uniformContinuous_dom₂
uniformity_eq 📖	mathematical	—	uniformity SeparationQuotient UniformSpace.toTopologicalSpace instUniformSpace Filter.map	—	—

UniformSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
completelyNormalSpace_of_hasAntitoneBasis 📖	mathematical	Filter.HasAntitoneBasis PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder uniformity	CompletelyNormalSpace toTopologicalSpace	—	Disjoint.symm mem_nhds_iff nhds_le_nhdsSet Filter.disjoint_principal_right disjoint_nhdsSet_principal comp_symm_mem_uniformity_sets Filter.HasAntitoneBasis.mem_iff Set.subset_compl_iff_disjoint_right subset_trans Set.instIsTransSubset ball_mono SetRel.comp_subset_comp SetRel.inv_mono SetRel.inv_eq_self mem_nhdsSet_iff_forall Filter.mem_of_superset ball_mem_nhds Filter.HasAntitoneBasis.mem Set.subset_iUnion Filter.disjoint_iff Set.disjoint_iff Disjoint.notMem_of_mem_left mem_ball_comp Filter.HasAntitoneBasis.antitone le_total
completelyNormalSpace_of_isCountablyGenerated_uniformity 📖	mathematical	—	CompletelyNormalSpace toTopologicalSpace	—	has_seq_basis completelyNormalSpace_of_hasAntitoneBasis
to_regularSpace 📖	mathematical	—	RegularSpace toTopologicalSpace	—	RegularSpace.of_hasBasis nhds_basis_uniformity' uniformity_hasBasis_closed isClosed_ball

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_of_clusterPt_uniformity 📖	—	—	—	—	Inseparable.eq inseparable_iff_clusterPt_uniformity
eq_of_forall_symmetric 📖	—	Set Set.instMembership	—	—	eq_of_uniformity_basis UniformSpace.hasBasis_symmetric
eq_of_uniformity 📖	—	Set Set.instMembership	—	—	t0Space_iff_uniformity
eq_of_uniformity_basis 📖	—	Filter.HasBasis uniformity Set Set.instMembership	—	—	Inseparable.eq Filter.HasBasis.inseparable_iff_uniformity
inseparable_iff_clusterPt_uniformity 📖	mathematical	—	Inseparable UniformSpace.toTopologicalSpace ClusterPt instTopologicalSpaceProd uniformity	—	ClusterPt.of_nhds_le Inseparable.nhds_le_uniformity Filter.HasBasis.inseparable_iff_uniformity uniformity_hasBasis_closed ClusterPt.mono Filter.le_principal_iff
inseparable_iff_ker_uniformity 📖	mathematical	—	Inseparable UniformSpace.toTopologicalSpace Set Set.instMembership Filter.ker uniformity	—	Filter.HasBasis.inseparable_iff_uniformity Filter.basis_sets
isClosed_of_spaced_out 📖	mathematical	Set Filter Filter.instMembership uniformity Set.Pairwise Set.instMembership	IsClosed UniformSpace.toTopologicalSpace	—	comp_symm_mem_uniformity_sets isClosed_of_closure_subset UniformSpace.mem_closure_iff_ball eq_of_forall_symmetric Filter.inter_mem UniformSpace.ball_inter_right UniformSpace.mem_comp_of_mem_ball UniformSpace.ball_inter_left
isClosed_range_of_spaced_out 📖	mathematical	Set Filter Filter.instMembership uniformity Pairwise Set.instMembership	IsClosed UniformSpace.toTopologicalSpace Set.range	—	isClosed_of_spaced_out
t0Space_iff_ker_uniformity 📖	mathematical	—	T0Space UniformSpace.toTopologicalSpace Filter.ker uniformity Set.diagonal	—	Set.instReflSubset Set.instAntisymmSubset refl_mem_uniformity
t0Space_iff_uniformity 📖	mathematical	—	T0Space UniformSpace.toTopologicalSpace	—	—
t0Space_iff_uniformity' 📖	mathematical	—	T0Space UniformSpace.toTopologicalSpace Pairwise Set Filter Filter.instMembership uniformity Set.instMembership	—	—

---

← Back to Index