case intro.intro.intro.intro.intro.intro.intro
α✝ : Type u
β : Type v
ι : Type ?u.136399
π : ι → Type ?u.136404
inst✝² : TopologicalSpace α✝
s t u v : Set α✝
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TotallySeparatedSpace α
x y : α
hxy : x ≠ y
U V : Set α
hU : IsOpen U
hV : IsOpen V
Ux : x ∈ U
Vy : y ∈ V
f : univ ⊆ U ∪ V
disj : Disjoint U V
⊢ ∃ U, IsClopen U ∧ x ∈ U ∧ y ∈ Uᶜ
α✝ : Type u
β : Type v
ι : Type ?u.136399
π : ι → Type ?u.136404
inst✝² : TopologicalSpace α✝
s t u v : Set α✝
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TotallySeparatedSpace α
x y : α
hxy : x ≠ y
⊢ ∃ U, IsClopen U ∧ x ∈ U ∧ y ∈ Uᶜ
obtain ⟨U, V, hU, hV, Ux, Vy, f, disj⟩ :=
  TotallySeparatedSpace.isTotallySeparated_univ x (Set.mem_univ x) y (Set.mem_univ y) hxy
case intro.intro.intro.intro.intro.intro.intro
α✝ : Type u
β : Type v
ι : Type ?u.136399
π : ι → Type ?u.136404
inst✝² : TopologicalSpace α✝
s t u v : Set α✝
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TotallySeparatedSpace α
x y : α
hxy : x ≠ y
U V : Set α
hU : IsOpen U
hV : IsOpen V
Ux : x ∈ U
Vy : y ∈ V
f : univ ⊆ U ∪ V
disj : Disjoint U V
clopen_U : IsClopen (univ ∩ U)
⊢ ∃ U, IsClopen U ∧ x ∈ U ∧ y ∈ Uᶜ
case intro.intro.intro.intro.intro.intro.intro
α✝ : Type u
β : Type v
ι : Type ?u.136399
π : ι → Type ?u.136404
inst✝² : TopologicalSpace α✝
s t u v : Set α✝
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TotallySeparatedSpace α
x y : α
hxy : x ≠ y
U V : Set α
hU : IsOpen U
hV : IsOpen V
Ux : x ∈ U
Vy : y ∈ V
f : univ ⊆ U ∪ V
disj : Disjoint U V
⊢ ∃ U, IsClopen U ∧ x ∈ U ∧ y ∈ Uᶜ
have clopen_U := isClopen_inter_of_disjoint_cover_clopen isClopen_univ f hU hV disj
case intro.intro.intro.intro.intro.intro.intro
α✝ : Type u
β : Type v
ι : Type ?u.136399
π : ι → Type ?u.136404
inst✝² : TopologicalSpace α✝
s t u v : Set α✝
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TotallySeparatedSpace α
x y : α
hxy : x ≠ y
U V : Set α
hU : IsOpen U
hV : IsOpen V
Ux : x ∈ U
Vy : y ∈ V
f : univ ⊆ U ∪ V
disj : Disjoint U V
clopen_U : IsClopen U
⊢ ∃ U, IsClopen U ∧ x ∈ U ∧ y ∈ Uᶜ
case intro.intro.intro.intro.intro.intro.intro
α✝ : Type u
β : Type v
ι : Type ?u.136399
π : ι → Type ?u.136404
inst✝² : TopologicalSpace α✝
s t u v : Set α✝
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TotallySeparatedSpace α
x y : α
hxy : x ≠ y
U V : Set α
hU : IsOpen U
hV : IsOpen V
Ux : x ∈ U
Vy : y ∈ V
f : univ ⊆ U ∪ V
disj : Disjoint U V
clopen_U : IsClopen (univ ∩ U)
⊢ ∃ U, IsClopen U ∧ x ∈ U ∧ y ∈ Uᶜ
rw [univ_inter _] at clopen_U
case intro.intro.intro.intro.intro.intro.intro
α✝ : Type u
β : Type v
ι : Type ?u.136399
π : ι → Type ?u.136404
inst✝² : TopologicalSpace α✝
s t u v : Set α✝
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TotallySeparatedSpace α
x y : α
hxy : x ≠ y
U V : Set α
hU : IsOpen U
hV : IsOpen V
Ux : x ∈ U
Vy : y ∈ V
f : univ ⊆ U ∪ V
disj : V ⊆ Uᶜ
clopen_U : IsClopen U
⊢ ∃ U, IsClopen U ∧ x ∈ U ∧ y ∈ Uᶜ
case intro.intro.intro.intro.intro.intro.intro
α✝ : Type u
β : Type v
ι : Type ?u.136399
π : ι → Type ?u.136404
inst✝² : TopologicalSpace α✝
s t u v : Set α✝
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TotallySeparatedSpace α
x y : α
hxy : x ≠ y
U V : Set α
hU : IsOpen U
hV : IsOpen V
Ux : x ∈ U
Vy : y ∈ V
f : univ ⊆ U ∪ V
disj : Disjoint U V
clopen_U : IsClopen U
⊢ ∃ U, IsClopen U ∧ x ∈ U ∧ y ∈ Uᶜ
rw [← Set.subset_compl_iff_disjoint_right, subset_compl_comm] at disj
no goals
case intro.intro.intro.intro.intro.intro.intro
α✝ : Type u
β : Type v
ι : Type ?u.136399
π : ι → Type ?u.136404
inst✝² : TopologicalSpace α✝
s t u v : Set α✝
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TotallySeparatedSpace α
x y : α
hxy : x ≠ y
U V : Set α
hU : IsOpen U
hV : IsOpen V
Ux : x ∈ U
Vy : y ∈ V
f : univ ⊆ U ∪ V
disj : V ⊆ Uᶜ
clopen_U : IsClopen U
⊢ ∃ U, IsClopen U ∧ x ∈ U ∧ y ∈ Uᶜ
exact ⟨U, clopen_U, Ux, disj Vy⟩