Theorems · Theorem · general topology

Topology.IsEmbedding.isTotallyDisconnected_range

∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β},
  Topology.IsEmbedding f → (IsTotallyDisconnected (Set.range f) ↔ TotallyDisconnectedSpace α)

Defined in: Mathlib.Topology.Connected.TotallyDisconnected
Cited by: 2 results in Mathlib
Foundations: Depth 81 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: TopologicalSpace TopologicalSpace

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites10

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Setproof · cited by 53,352
TopologicalSpacestatement and proof · cited by 24,529
Set.rangestatement and proof · cited by 4,705
Set.univproof · cited by 3,945
Set.image_univproof · cited by 322
TotallyDisconnectedSpacestatement · cited by 295
Topology.IsEmbeddingstatement and proof · cited by 294
IsTotallyDisconnectedstatement and proof · cited by 14
totallyDisconnectedSpace_iffproof · cited by 2
Topology.IsEmbedding.isTotallyDisconnected_imageproof · cited by 1

Cited by2

Results whose statement or proof uses this declaration.

totallyDisconnectedSpace_subtype_iffproof · cited by 1
Homeomorph.totallyDisconnectedSpaceproof · cited by 0