α : Type u
β : Type v
ι : Type ?u.120754
π : ι → Type ?u.120759
inst✝¹ : TopologicalSpace α
s t u v : Set α
X : Type u_1
inst✝ : TopologicalSpace X
hX : Pairwise fun x y => ∃ U, IsClopen U ∧ x ∈ U ∧ ¬y ∈ U
S : Set X
hS : IsPreconnected S
⊢ Set.Subsingleton S
α : Type u
β : Type v
ι : Type ?u.120754
π : ι → Type ?u.120759
inst✝¹ : TopologicalSpace α
s t u v : Set α
X : Type u_1
inst✝ : TopologicalSpace X
hX : Pairwise fun x y => ∃ U, IsClopen U ∧ x ∈ U ∧ ¬y ∈ U
⊢ IsTotallyDisconnected univ
rintro S - hS
α : Type u
β : Type v
ι : Type ?u.120754
π : ι → Type ?u.120759
inst✝¹ : TopologicalSpace α
s t u v : Set α
X : Type u_1
inst✝ : TopologicalSpace X
hX : Pairwise fun x y => ∃ U, IsClopen U ∧ x ∈ U ∧ ¬y ∈ U
S : Set X
hS : IsPreconnected S
⊢ ∀ ⦃x : X⦄, x ∈ S → ∀ ⦃y : X⦄, y ∈ S → x = y
α : Type u
β : Type v
ι : Type ?u.120754
π : ι → Type ?u.120759
inst✝¹ : TopologicalSpace α
s t u v : Set α
X : Type u_1
inst✝ : TopologicalSpace X
hX : Pairwise fun x y => ∃ U, IsClopen U ∧ x ∈ U ∧ ¬y ∈ U
S : Set X
hS : IsPreconnected S
⊢ Set.Subsingleton S
unfold Set.Subsingleton
α : Type u
β : Type v
ι : Type ?u.120754
π : ι → Type ?u.120759
inst✝¹ : TopologicalSpace α
s t u v : Set α
X : Type u_1
inst✝ : TopologicalSpace X
hX : Pairwise fun x y => ∃ U, IsClopen U ∧ x ∈ U ∧ ¬y ∈ U
S : Set X
hS : IsPreconnected S
h_contra : Exists fun ⦃x⦄ => x ∈ S ∧ Exists fun ⦃y⦄ => y ∈ S ∧ x ≠ y
⊢ False
α : Type u
β : Type v
ι : Type ?u.120754
π : ι → Type ?u.120759
inst✝¹ : TopologicalSpace α
s t u v : Set α
X : Type u_1
inst✝ : TopologicalSpace X
hX : Pairwise fun x y => ∃ U, IsClopen U ∧ x ∈ U ∧ ¬y ∈ U
S : Set X
hS : IsPreconnected S
⊢ ∀ ⦃x : X⦄, x ∈ S → ∀ ⦃y : X⦄, y ∈ S → x = y
by_contra' h_contra
case intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.120754
π : ι → Type ?u.120759
inst✝¹ : TopologicalSpace α
s t u v : Set α
X : Type u_1
inst✝ : TopologicalSpace X
hX : Pairwise fun x y => ∃ U, IsClopen U ∧ x ∈ U ∧ ¬y ∈ U
S : Set X
hS : IsPreconnected S
x : X
hx : x ∈ S
y : X
hy : y ∈ S
hxy : x ≠ y
⊢ False
α : Type u
β : Type v
ι : Type ?u.120754
π : ι → Type ?u.120759
inst✝¹ : TopologicalSpace α
s t u v : Set α
X : Type u_1
inst✝ : TopologicalSpace X
hX : Pairwise fun x y => ∃ U, IsClopen U ∧ x ∈ U ∧ ¬y ∈ U
S : Set X
hS : IsPreconnected S
h_contra : Exists fun ⦃x⦄ => x ∈ S ∧ Exists fun ⦃y⦄ => y ∈ S ∧ x ≠ y
⊢ False
rcases h_contra with ⟨x, hx, y, hy, hxy⟩
case intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.120754
π : ι → Type ?u.120759
inst✝¹ : TopologicalSpace α
s t u v : Set α
X : Type u_1
inst✝ : TopologicalSpace X
hX : Pairwise fun x y => ∃ U, IsClopen U ∧ x ∈ U ∧ ¬y ∈ U
S : Set X
hS : IsPreconnected S
x : X
hx : x ∈ S
y : X
hy : y ∈ S
hxy : x ≠ y
U : Set X
h_clopen : IsClopen U
hxU : x ∈ U
hyU : ¬y ∈ U
⊢ False
case intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.120754
π : ι → Type ?u.120759
inst✝¹ : TopologicalSpace α
s t u v : Set α
X : Type u_1
inst✝ : TopologicalSpace X
hX : Pairwise fun x y => ∃ U, IsClopen U ∧ x ∈ U ∧ ¬y ∈ U
S : Set X
hS : IsPreconnected S
x : X
hx : x ∈ S
y : X
hy : y ∈ S
hxy : x ≠ y
⊢ False
obtain ⟨U, h_clopen, hxU, hyU⟩ := hX hxy
case intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.120754
π : ι → Type ?u.120759
inst✝¹ : TopologicalSpace α
s t u v : Set α
X : Type u_1
inst✝ : TopologicalSpace X
hX : Pairwise fun x y => ∃ U, IsClopen U ∧ x ∈ U ∧ ¬y ∈ U
S : Set X
x : X
hx : x ∈ S
y : X
hy : y ∈ S
hxy : x ≠ y
U : Set X
h_clopen : IsClopen U
hxU : x ∈ U
hyU : ¬y ∈ U
hS : Set.Nonempty (S ∩ (U ∩ Uᶜ))
⊢ False
case intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.120754
π : ι → Type ?u.120759
inst✝¹ : TopologicalSpace α
s t u v : Set α
X : Type u_1
inst✝ : TopologicalSpace X
hX : Pairwise fun x y => ∃ U, IsClopen U ∧ x ∈ U ∧ ¬y ∈ U
S : Set X
hS : IsPreconnected S
x : X
hx : x ∈ S
y : X
hy : y ∈ S
hxy : x ≠ y
U : Set X
h_clopen : IsClopen U
hxU : x ∈ U
hyU : ¬y ∈ U
⊢ False
specialize
  hS U (Uᶜ) h_clopen.1 h_clopen.compl.1 (fun a _ => em (a ∈ U)) ⟨x, hx, hxU⟩ ⟨y, hy, hyU⟩
case intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.120754
π : ι → Type ?u.120759
inst✝¹ : TopologicalSpace α
s t u v : Set α
X : Type u_1
inst✝ : TopologicalSpace X
hX : Pairwise fun x y => ∃ U, IsClopen U ∧ x ∈ U ∧ ¬y ∈ U
S : Set X
x : X
hx : x ∈ S
y : X
hy : y ∈ S
hxy : x ≠ y
U : Set X
h_clopen : IsClopen U
hxU : x ∈ U
hyU : ¬y ∈ U
hS : Set.Nonempty ∅
⊢ False
case intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.120754
π : ι → Type ?u.120759
inst✝¹ : TopologicalSpace α
s t u v : Set α
X : Type u_1
inst✝ : TopologicalSpace X
hX : Pairwise fun x y => ∃ U, IsClopen U ∧ x ∈ U ∧ ¬y ∈ U
S : Set X
x : X
hx : x ∈ S
y : X
hy : y ∈ S
hxy : x ≠ y
U : Set X
h_clopen : IsClopen U
hxU : x ∈ U
hyU : ¬y ∈ U
hS : Set.Nonempty (S ∩ (U ∩ Uᶜ))
⊢ False
rw [inter_compl_self, Set.inter_empty] at hS
no goals
case intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.120754
π : ι → Type ?u.120759
inst✝¹ : TopologicalSpace α
s t u v : Set α
X : Type u_1
inst✝ : TopologicalSpace X
hX : Pairwise fun x y => ∃ U, IsClopen U ∧ x ∈ U ∧ ¬y ∈ U
S : Set X
x : X
hx : x ∈ S
y : X
hy : y ∈ S
hxy : x ≠ y
U : Set X
h_clopen : IsClopen U
hxU : x ∈ U
hyU : ¬y ∈ U
hS : Set.Nonempty ∅
⊢ False
exact Set.not_nonempty_empty hS