CompleteSeparated

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

Statistics

Metric	Count
Definitions	0
Theorems isClosed, continuous_extend_of_cauchy, isClosedEmbedding	3
Total	3

IsComplete

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isClosed 📖	mathematical	IsComplete	IsClosed UniformSpace.toTopologicalSpace	—	isClosed_iff_clusterPt Cauchy.mono' cauchy_nhds inf_le_left inf_le_right tendsto_nhds_unique' T25Space.t2Space T3Space.t25Space instT3Space UniformSpace.to_regularSpace

IsDenseInducing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuous_extend_of_cauchy 📖	mathematical	IsDenseInducing Cauchy Filter.map Filter.comap nhds	Continuous UniformSpace.toTopologicalSpace extend	—	continuous_extend instT3Space UniformSpace.to_regularSpace CompleteSpace.complete

IsUniformEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isClosedEmbedding 📖	mathematical	IsUniformEmbedding	Topology.IsClosedEmbedding UniformSpace.toTopologicalSpace	—	isEmbedding IsComplete.isClosed IsUniformInducing.isComplete_range isUniformInducing

---

← Back to Index