α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : CompactSpace α
h : TotallyDisconnectedSpace α
x : α
x✝¹ : x ∈ univ
y : α
x✝ : y ∈ univ
⊢ x ≠ y → ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : CompactSpace α
⊢ TotallyDisconnectedSpace α ↔ TotallySeparatedSpace α
refine ⟨fun h => ⟨fun x _ y _ => ?_⟩, @TotallySeparatedSpace.totallyDisconnectedSpace _ _⟩
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : CompactSpace α
h : TotallyDisconnectedSpace α
x : α
x✝¹ : x ∈ univ
y : α
x✝ : y ∈ univ
⊢ (∀ (u v : Set α), IsOpen u → IsOpen v → x ∈ u → y ∈ v → univ ⊆ u ∪ v → ¬Disjoint u v) → x = y
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : CompactSpace α
h : TotallyDisconnectedSpace α
x : α
x✝¹ : x ∈ univ
y : α
x✝ : y ∈ univ
⊢ x ≠ y → ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v
contrapose!
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : CompactSpace α
h : TotallyDisconnectedSpace α
x : α
x✝¹ : x ∈ univ
y : α
x✝ : y ∈ univ
hyp : ∀ (u v : Set α), IsOpen u → IsOpen v → x ∈ u → y ∈ v → univ ⊆ u ∪ v → ¬Disjoint u v
⊢ x = y
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : CompactSpace α
h : TotallyDisconnectedSpace α
x : α
x✝¹ : x ∈ univ
y : α
x✝ : y ∈ univ
⊢ (∀ (u v : Set α), IsOpen u → IsOpen v → x ∈ u → y ∈ v → univ ⊆ u ∪ v → ¬Disjoint u v) → x = y
intro hyp
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : CompactSpace α
h : TotallyDisconnectedSpace α
x : α
x✝¹ : x ∈ univ
y : α
x✝ : y ∈ univ
hyp : ∀ (u v : Set α), IsOpen u → IsOpen v → x ∈ u → y ∈ v → univ ⊆ u ∪ v → ¬Disjoint u v
⊢ x ∈ connectedComponent y
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : CompactSpace α
h : TotallyDisconnectedSpace α
x : α
x✝¹ : x ∈ univ
y : α
x✝ : y ∈ univ
hyp : ∀ (u v : Set α), IsOpen u → IsOpen v → x ∈ u → y ∈ v → univ ⊆ u ∪ v → ¬Disjoint u v
⊢ x = y
suffices x ∈ connectedComponent y by
  simpa [totallyDisconnectedSpace_iff_connectedComponent_singleton.1 h y, mem_singleton_iff]
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : CompactSpace α
h : TotallyDisconnectedSpace α
x : α
x✝¹ : x ∈ univ
y : α
x✝ : y ∈ univ
hyp : ∀ (u v : Set α), IsOpen u → IsOpen v → x ∈ u → y ∈ v → univ ⊆ u ∪ v → ¬Disjoint u v
⊢ ∀ (i : { Z // IsClopen Z ∧ y ∈ Z }), x ∈ ↑i
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : CompactSpace α
h : TotallyDisconnectedSpace α
x : α
x✝¹ : x ∈ univ
y : α
x✝ : y ∈ univ
hyp : ∀ (u v : Set α), IsOpen u → IsOpen v → x ∈ u → y ∈ v → univ ⊆ u ∪ v → ¬Disjoint u v
⊢ x ∈ connectedComponent y
rw [connectedComponent_eq_iInter_clopen, mem_iInter]
case mk.intro
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : CompactSpace α
h : TotallyDisconnectedSpace α
x : α
x✝¹ : x ∈ univ
y : α
x✝ : y ∈ univ
hyp : ∀ (u v : Set α), IsOpen u → IsOpen v → x ∈ u → y ∈ v → univ ⊆ u ∪ v → ¬Disjoint u v
w : Set α
hw : IsClopen w
hy : y ∈ w
⊢ x ∈ ↑{ val := w, property := (_ : IsClopen w ∧ y ∈ w) }
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : CompactSpace α
h : TotallyDisconnectedSpace α
x : α
x✝¹ : x ∈ univ
y : α
x✝ : y ∈ univ
hyp : ∀ (u v : Set α), IsOpen u → IsOpen v → x ∈ u → y ∈ v → univ ⊆ u ∪ v → ¬Disjoint u v
⊢ ∀ (i : { Z // IsClopen Z ∧ y ∈ Z }), x ∈ ↑i
rintro ⟨w : Set α, hw : IsClopen w, hy : y ∈ w⟩
case mk.intro
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : CompactSpace α
h : TotallyDisconnectedSpace α
x : α
x✝¹ : x ∈ univ
y : α
x✝ : y ∈ univ
hyp : ∀ (u v : Set α), IsOpen u → IsOpen v → x ∈ u → y ∈ v → univ ⊆ u ∪ v → ¬Disjoint u v
w : Set α
hw : IsClopen w
hy : y ∈ w
hx : ¬x ∈ ↑{ val := w, property := (_ : IsClopen w ∧ y ∈ w) }
⊢ False
case mk.intro
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : CompactSpace α
h : TotallyDisconnectedSpace α
x : α
x✝¹ : x ∈ univ
y : α
x✝ : y ∈ univ
hyp : ∀ (u v : Set α), IsOpen u → IsOpen v → x ∈ u → y ∈ v → univ ⊆ u ∪ v → ¬Disjoint u v
w : Set α
hw : IsClopen w
hy : y ∈ w
⊢ x ∈ ↑{ val := w, property := (_ : IsClopen w ∧ y ∈ w) }
by_contra hx
no goals
case mk.intro
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : CompactSpace α
h : TotallyDisconnectedSpace α
x : α
x✝¹ : x ∈ univ
y : α
x✝ : y ∈ univ
hyp : ∀ (u v : Set α), IsOpen u → IsOpen v → x ∈ u → y ∈ v → univ ⊆ u ∪ v → ¬Disjoint u v
w : Set α
hw : IsClopen w
hy : y ∈ w
hx : ¬x ∈ ↑{ val := w, property := (_ : IsClopen w ∧ y ∈ w) }
⊢ False
exact hyp (wᶜ) w hw.2.isOpen_compl hw.1 hx hy (@isCompl_compl _ w _).symm.codisjoint.top_le
  disjoint_compl_left
no goals
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : CompactSpace α
h : TotallyDisconnectedSpace α
x : α
x✝¹ : x ∈ univ
y : α
x✝ : y ∈ univ
hyp : ∀ (u v : Set α), IsOpen u → IsOpen v → x ∈ u → y ∈ v → univ ⊆ u ∪ v → ¬Disjoint u v
this : x ∈ connectedComponent y
⊢ x = y
simpa [totallyDisconnectedSpace_iff_connectedComponent_singleton.1 h y, mem_singleton_iff]