case isTotallySeparated_univ
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
h : IsTopologicalBasis {s | IsClopen s}
⊢ IsTotallySeparated univ
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
h : IsTopologicalBasis {s | IsClopen s}
⊢ TotallySeparatedSpace α
constructor
case isTotallySeparated_univ
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
h : IsTopologicalBasis {s | IsClopen s}
x y : α
hxy : x ≠ y
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v
case isTotallySeparated_univ
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
h : IsTopologicalBasis {s | IsClopen s}
⊢ IsTotallySeparated univ
rintro x - y - hxy
case isTotallySeparated_univ.intro.intro.intro
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
h : IsTopologicalBasis {s | IsClopen s}
x y : α
hxy : x ≠ y
U : Set α
hU : U ∈ {s | IsClopen s}
hxU : x ∈ U
hyU : U ⊆ {y_1 | y_1 ≠ y}
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v
case isTotallySeparated_univ
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
h : IsTopologicalBasis {s | IsClopen s}
x y : α
hxy : x ≠ y
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v
rcases h.mem_nhds_iff.mp (isOpen_ne.mem_nhds hxy) with ⟨U, hU, hxU, hyU⟩
no goals
case isTotallySeparated_univ.intro.intro.intro
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
h : IsTopologicalBasis {s | IsClopen s}
x y : α
hxy : x ≠ y
U : Set α
hU : U ∈ {s | IsClopen s}
hxU : x ∈ U
hyU : U ⊆ {y_1 | y_1 ≠ y}
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v
exact ⟨U, Uᶜ, hU.isOpen, hU.compl.isOpen, hxU, fun h => hyU h rfl, (union_compl_self U).superset,
  disjoint_compl_right⟩