α : Type u
β : Type v
ι : Type ?u.134712
π : ι → Type ?u.134717
inst✝ : TopologicalSpace α
s✝ t✝ u v s : Set α
H : IsTotallySeparated s
t : Set α
hts : t ⊆ s
ht : IsPreconnected t
x : α
x_in : x ∈ t
y : α
y_in : y ∈ t
⊢ x = y
α : Type u
β : Type v
ι : Type ?u.134712
π : ι → Type ?u.134717
inst✝ : TopologicalSpace α
s✝ t u v s : Set α
H : IsTotallySeparated s
⊢ IsTotallyDisconnected s
intro t hts ht x x_in y y_in
α : Type u
β : Type v
ι : Type ?u.134712
π : ι → Type ?u.134717
inst✝ : TopologicalSpace α
s✝ t✝ u v s : Set α
H : IsTotallySeparated s
t : Set α
hts : t ⊆ s
ht : IsPreconnected t
x : α
x_in : x ∈ t
y : α
y_in : y ∈ t
h : ¬x = y
⊢ False
α : Type u
β : Type v
ι : Type ?u.134712
π : ι → Type ?u.134717
inst✝ : TopologicalSpace α
s✝ t✝ u v s : Set α
H : IsTotallySeparated s
t : Set α
hts : t ⊆ s
ht : IsPreconnected t
x : α
x_in : x ∈ t
y : α
y_in : y ∈ t
⊢ x = y
by_contra h
case intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.134712
π : ι → Type ?u.134717
inst✝ : TopologicalSpace α
s✝ t✝ u✝ v✝ s : Set α
H : IsTotallySeparated s
t : Set α
hts : t ⊆ s
ht : IsPreconnected t
x : α
x_in : x ∈ t
y : α
y_in : y ∈ t
h : ¬x = y
u v : Set α
hu : IsOpen u
hv : IsOpen v
hxu : x ∈ u
hyv : y ∈ v
hs : s ⊆ u ∪ v
huv : Disjoint u v
⊢ False
α : Type u
β : Type v
ι : Type ?u.134712
π : ι → Type ?u.134717
inst✝ : TopologicalSpace α
s✝ t✝ u v s : Set α
H : IsTotallySeparated s
t : Set α
hts : t ⊆ s
ht : IsPreconnected t
x : α
x_in : x ∈ t
y : α
y_in : y ∈ t
h : ¬x = y
⊢ False
obtain
  ⟨u : Set α, v : Set α, hu : IsOpen u, hv : IsOpen v, hxu : x ∈ u, hyv : y ∈ v, hs : s ⊆ u ∪ v,
    huv⟩ :=
  H x (hts x_in) y (hts y_in) h
case intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.134712
π : ι → Type ?u.134717
inst✝ : TopologicalSpace α
s✝ t✝ u✝ v✝ s : Set α
H : IsTotallySeparated s
t : Set α
hts : t ⊆ s
ht : IsPreconnected t
x : α
x_in : x ∈ t
y : α
y_in : y ∈ t
h : ¬x = y
u v : Set α
hu : IsOpen u
hv : IsOpen v
hxu : x ∈ u
hyv : y ∈ v
hs : s ⊆ u ∪ v
huv : Disjoint u v
⊢ t ∩ (u ∩ v) = ∅
case intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.134712
π : ι → Type ?u.134717
inst✝ : TopologicalSpace α
s✝ t✝ u✝ v✝ s : Set α
H : IsTotallySeparated s
t : Set α
hts : t ⊆ s
ht : IsPreconnected t
x : α
x_in : x ∈ t
y : α
y_in : y ∈ t
h : ¬x = y
u v : Set α
hu : IsOpen u
hv : IsOpen v
hxu : x ∈ u
hyv : y ∈ v
hs : s ⊆ u ∪ v
huv : Disjoint u v
⊢ False
refine' (ht _ _ hu hv (hts.trans hs) ⟨x, x_in, hxu⟩ ⟨y, y_in, hyv⟩).ne_empty _
no goals
case intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.134712
π : ι → Type ?u.134717
inst✝ : TopologicalSpace α
s✝ t✝ u✝ v✝ s : Set α
H : IsTotallySeparated s
t : Set α
hts : t ⊆ s
ht : IsPreconnected t
x : α
x_in : x ∈ t
y : α
y_in : y ∈ t
h : ¬x = y
u v : Set α
hu : IsOpen u
hv : IsOpen v
hxu : x ∈ u
hyv : y ∈ v
hs : s ⊆ u ∪ v
huv : Disjoint u v
⊢ t ∩ (u ∩ v) = ∅
rw [huv.inter_eq, inter_empty]