case mp
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : CompactSpace α
inst✝ : TotallyDisconnectedSpace α
x : α
U : Set α
⊢ U ∈ 𝓝 x → ∃ i, (x ∈ i ∧ IsClopen i) ∧ id i ⊆ U

case mpr
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : CompactSpace α
inst✝ : TotallyDisconnectedSpace α
x : α
U : Set α
⊢ (∃ i, (x ∈ i ∧ IsClopen i) ∧ id i ⊆ U) → U ∈ 𝓝 x
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : CompactSpace α
inst✝ : TotallyDisconnectedSpace α
x : α
U : Set α
⊢ U ∈ 𝓝 x ↔ ∃ i, (x ∈ i ∧ IsClopen i) ∧ id i ⊆ U
constructor
case mp
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : CompactSpace α
inst✝ : TotallyDisconnectedSpace α
x : α
U : Set α
hx : connectedComponent x = {x}
⊢ U ∈ 𝓝 x → ∃ i, (x ∈ i ∧ IsClopen i) ∧ id i ⊆ U
case mp
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : CompactSpace α
inst✝ : TotallyDisconnectedSpace α
x : α
U : Set α
⊢ U ∈ 𝓝 x → ∃ i, (x ∈ i ∧ IsClopen i) ∧ id i ⊆ U
have hx : connectedComponent x = {x} :=
  totallyDisconnectedSpace_iff_connectedComponent_singleton.mp ‹_› x
case mp
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : CompactSpace α
inst✝ : TotallyDisconnectedSpace α
x : α
U : Set α
hx : (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) = {x}
⊢ U ∈ 𝓝 x → ∃ i, (x ∈ i ∧ IsClopen i) ∧ id i ⊆ U
case mp
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : CompactSpace α
inst✝ : TotallyDisconnectedSpace α
x : α
U : Set α
hx : connectedComponent x = {x}
⊢ U ∈ 𝓝 x → ∃ i, (x ∈ i ∧ IsClopen i) ∧ id i ⊆ U
rw [connectedComponent_eq_iInter_clopen] at hx
case mp
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : CompactSpace α
inst✝ : TotallyDisconnectedSpace α
x : α
U : Set α
hx : (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) = {x}
hU : U ∈ 𝓝 x
⊢ ∃ i, (x ∈ i ∧ IsClopen i) ∧ id i ⊆ U
case mp
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : CompactSpace α
inst✝ : TotallyDisconnectedSpace α
x : α
U : Set α
hx : (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) = {x}
⊢ U ∈ 𝓝 x → ∃ i, (x ∈ i ∧ IsClopen i) ∧ id i ⊆ U
intro hU
case mp
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : CompactSpace α
inst✝ : TotallyDisconnectedSpace α
x : α
U : Set α
hx : (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) = {x}
hU : U ∈ 𝓝 x
N : Type u := { Z // IsClopen Z ∧ x ∈ Z }
⊢ ∃ i, (x ∈ i ∧ IsClopen i) ∧ id i ⊆ U
case mp
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : CompactSpace α
inst✝ : TotallyDisconnectedSpace α
x : α
U : Set α
hx : (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) = {x}
hU : U ∈ 𝓝 x
⊢ ∃ i, (x ∈ i ∧ IsClopen i) ∧ id i ⊆ U
let N := { Z // IsClopen Z ∧ x ∈ Z }
case mp
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : CompactSpace α
inst✝ : TotallyDisconnectedSpace α
x : α
U : Set α
hx : (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) = {x}
hU : U ∈ 𝓝 x
N : Type u := { Z // IsClopen Z ∧ x ∈ Z }
this : ∃ Z, ↑Z ⊆ U
⊢ ∃ i, (x ∈ i ∧ IsClopen i) ∧ id i ⊆ U

case this
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : CompactSpace α
inst✝ : TotallyDisconnectedSpace α
x : α
U : Set α
hx : (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) = {x}
hU : U ∈ 𝓝 x
N : Type u := { Z // IsClopen Z ∧ x ∈ Z }
⊢ ∃ Z, ↑Z ⊆ U
case mp
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : CompactSpace α
inst✝ : TotallyDisconnectedSpace α
x : α
U : Set α
hx : (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) = {x}
hU : U ∈ 𝓝 x
N : Type u := { Z // IsClopen Z ∧ x ∈ Z }
⊢ ∃ i, (x ∈ i ∧ IsClopen i) ∧ id i ⊆ U
suffices : ∃ Z : N, Z.val ⊆ U
case this
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : CompactSpace α
inst✝ : TotallyDisconnectedSpace α
x : α
U : Set α
hx : (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) = {x}
hU : U ∈ 𝓝 x
N : Type u := { Z // IsClopen Z ∧ x ∈ Z }
this : Nonempty N
⊢ ∃ Z, ↑Z ⊆ U
case this
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : CompactSpace α
inst✝ : TotallyDisconnectedSpace α
x : α
U : Set α
hx : (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) = {x}
hU : U ∈ 𝓝 x
N : Type u := { Z // IsClopen Z ∧ x ∈ Z }
⊢ ∃ Z, ↑Z ⊆ U
haveI : Nonempty N := ⟨⟨univ, isClopen_univ, mem_univ x⟩⟩
case this
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : CompactSpace α
inst✝ : TotallyDisconnectedSpace α
x : α
U : Set α
hx : (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) = {x}
hU : U ∈ 𝓝 x
N : Type u := { Z // IsClopen Z ∧ x ∈ Z }
this : Nonempty N
hNcl : ∀ (Z : N), IsClosed ↑Z
⊢ ∃ Z, ↑Z ⊆ U
case this
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : CompactSpace α
inst✝ : TotallyDisconnectedSpace α
x : α
U : Set α
hx : (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) = {x}
hU : U ∈ 𝓝 x
N : Type u := { Z // IsClopen Z ∧ x ∈ Z }
this : Nonempty N
⊢ ∃ Z, ↑Z ⊆ U
have hNcl : ∀ Z : N, IsClosed Z.val := fun Z => Z.property.1.2
case this
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : CompactSpace α
inst✝ : TotallyDisconnectedSpace α
x : α
U : Set α
hx : (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) = {x}
hU : U ∈ 𝓝 x
N : Type u := { Z // IsClopen Z ∧ x ∈ Z }
this : Nonempty N
hNcl : ∀ (Z : N), IsClosed ↑Z
hdir : Directed Superset fun Z => ↑Z
⊢ ∃ Z, ↑Z ⊆ U
case this
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : CompactSpace α
inst✝ : TotallyDisconnectedSpace α
x : α
U : Set α
hx : (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) = {x}
hU : U ∈ 𝓝 x
N : Type u := { Z // IsClopen Z ∧ x ∈ Z }
this : Nonempty N
hNcl : ∀ (Z : N), IsClosed ↑Z
⊢ ∃ Z, ↑Z ⊆ U
have hdir : Directed Superset fun Z : N => Z.val := by
  rintro ⟨s, hs, hxs⟩ ⟨t, ht, hxt⟩
  exact ⟨⟨s ∩ t, hs.inter ht, ⟨hxs, hxt⟩⟩, inter_subset_left s t, inter_subset_right s t⟩
case this
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : CompactSpace α
inst✝ : TotallyDisconnectedSpace α
x : α
U : Set α
hx : (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) = {x}
hU : U ∈ 𝓝 x
N : Type u := { Z // IsClopen Z ∧ x ∈ Z }
this : Nonempty N
hNcl : ∀ (Z : N), IsClosed ↑Z
hdir : Directed Superset fun Z => ↑Z
h_nhd : ∀ (y : α), (y ∈ ⋂ (Z : N), ↑Z) → U ∈ 𝓝 y
⊢ ∃ Z, ↑Z ⊆ U
case this
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : CompactSpace α
inst✝ : TotallyDisconnectedSpace α
x : α
U : Set α
hx : (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) = {x}
hU : U ∈ 𝓝 x
N : Type u := { Z // IsClopen Z ∧ x ∈ Z }
this : Nonempty N
hNcl : ∀ (Z : N), IsClosed ↑Z
hdir : Directed Superset fun Z => ↑Z
⊢ ∃ Z, ↑Z ⊆ U
have h_nhd : ∀ y ∈ ⋂ Z : N, Z.val, U ∈ 𝓝 y := fun y y_in => by
  erw [hx, mem_singleton_iff] at y_in
  rwa [y_in]
no goals
case this
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : CompactSpace α
inst✝ : TotallyDisconnectedSpace α
x : α
U : Set α
hx : (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) = {x}
hU : U ∈ 𝓝 x
N : Type u := { Z // IsClopen Z ∧ x ∈ Z }
this : Nonempty N
hNcl : ∀ (Z : N), IsClosed ↑Z
hdir : Directed Superset fun Z => ↑Z
h_nhd : ∀ (y : α), (y ∈ ⋂ (Z : N), ↑Z) → U ∈ 𝓝 y
⊢ ∃ Z, ↑Z ⊆ U
exact exists_subset_nhds_of_compactSpace hdir hNcl h_nhd
case mp.intro.mk.intro
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : CompactSpace α
inst✝ : TotallyDisconnectedSpace α
x : α
U : Set α
hx : (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) = {x}
hU : U ∈ 𝓝 x
N : Type u := { Z // IsClopen Z ∧ x ∈ Z }
s : Set α
hs : IsClopen s
hs' : x ∈ s
hs'' : ↑{ val := s, property := (_ : IsClopen s ∧ x ∈ s) } ⊆ U
⊢ ∃ i, (x ∈ i ∧ IsClopen i) ∧ id i ⊆ U
case mp
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : CompactSpace α
inst✝ : TotallyDisconnectedSpace α
x : α
U : Set α
hx : (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) = {x}
hU : U ∈ 𝓝 x
N : Type u := { Z // IsClopen Z ∧ x ∈ Z }
this : ∃ Z, ↑Z ⊆ U
⊢ ∃ i, (x ∈ i ∧ IsClopen i) ∧ id i ⊆ U
rcases this with  ⟨⟨s, hs, hs'⟩, hs''⟩
no goals
case mp.intro.mk.intro
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : CompactSpace α
inst✝ : TotallyDisconnectedSpace α
x : α
U : Set α
hx : (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) = {x}
hU : U ∈ 𝓝 x
N : Type u := { Z // IsClopen Z ∧ x ∈ Z }
s : Set α
hs : IsClopen s
hs' : x ∈ s
hs'' : ↑{ val := s, property := (_ : IsClopen s ∧ x ∈ s) } ⊆ U
⊢ ∃ i, (x ∈ i ∧ IsClopen i) ∧ id i ⊆ U
exact ⟨s, ⟨hs', hs⟩, hs''⟩
case mk.intro.mk.intro
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : CompactSpace α
inst✝ : TotallyDisconnectedSpace α
x : α
U : Set α
hx : (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) = {x}
hU : U ∈ 𝓝 x
N : Type u := { Z // IsClopen Z ∧ x ∈ Z }
this : Nonempty N
hNcl : ∀ (Z : N), IsClosed ↑Z
s : Set α
hs : IsClopen s
hxs : x ∈ s
t : Set α
ht : IsClopen t
hxt : x ∈ t
⊢ ∃ z,
    (fun Z => ↑Z) { val := s, property := (_ : IsClopen s ∧ x ∈ s) } ⊇ (fun Z => ↑Z) z ∧
      (fun Z => ↑Z) { val := t, property := (_ : IsClopen t ∧ x ∈ t) } ⊇ (fun Z => ↑Z) z
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : CompactSpace α
inst✝ : TotallyDisconnectedSpace α
x : α
U : Set α
hx : (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) = {x}
hU : U ∈ 𝓝 x
N : Type u := { Z // IsClopen Z ∧ x ∈ Z }
this : Nonempty N
hNcl : ∀ (Z : N), IsClosed ↑Z
⊢ Directed Superset fun Z => ↑Z
rintro ⟨s, hs, hxs⟩ ⟨t, ht, hxt⟩
no goals
case mk.intro.mk.intro
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : CompactSpace α
inst✝ : TotallyDisconnectedSpace α
x : α
U : Set α
hx : (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) = {x}
hU : U ∈ 𝓝 x
N : Type u := { Z // IsClopen Z ∧ x ∈ Z }
this : Nonempty N
hNcl : ∀ (Z : N), IsClosed ↑Z
s : Set α
hs : IsClopen s
hxs : x ∈ s
t : Set α
ht : IsClopen t
hxt : x ∈ t
⊢ ∃ z,
    (fun Z => ↑Z) { val := s, property := (_ : IsClopen s ∧ x ∈ s) } ⊇ (fun Z => ↑Z) z ∧
      (fun Z => ↑Z) { val := t, property := (_ : IsClopen t ∧ x ∈ t) } ⊇ (fun Z => ↑Z) z
exact ⟨⟨s ∩ t, hs.inter ht, ⟨hxs, hxt⟩⟩, inter_subset_left s t, inter_subset_right s t⟩
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : CompactSpace α
inst✝ : TotallyDisconnectedSpace α
x : α
U : Set α
hx : (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) = {x}
hU : U ∈ 𝓝 x
N : Type u := { Z // IsClopen Z ∧ x ∈ Z }
this : Nonempty N
hNcl : ∀ (Z : N), IsClosed ↑Z
hdir : Directed Superset fun Z => ↑Z
y : α
y_in : y = x
⊢ U ∈ 𝓝 y
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : CompactSpace α
inst✝ : TotallyDisconnectedSpace α
x : α
U : Set α
hx : (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) = {x}
hU : U ∈ 𝓝 x
N : Type u := { Z // IsClopen Z ∧ x ∈ Z }
this : Nonempty N
hNcl : ∀ (Z : N), IsClosed ↑Z
hdir : Directed Superset fun Z => ↑Z
y : α
y_in : y ∈ ⋂ (Z : N), ↑Z
⊢ U ∈ 𝓝 y
erw [hx, mem_singleton_iff] at y_in
no goals
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : CompactSpace α
inst✝ : TotallyDisconnectedSpace α
x : α
U : Set α
hx : (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) = {x}
hU : U ∈ 𝓝 x
N : Type u := { Z // IsClopen Z ∧ x ∈ Z }
this : Nonempty N
hNcl : ∀ (Z : N), IsClosed ↑Z
hdir : Directed Superset fun Z => ↑Z
y : α
y_in : y = x
⊢ U ∈ 𝓝 y
rwa [y_in]
case mpr.intro.intro.intro.intro
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : CompactSpace α
inst✝ : TotallyDisconnectedSpace α
x : α
U V : Set α
hUV : V ⊆ U
hxV : x ∈ V
V_op : IsOpen V
⊢ U ∈ 𝓝 x
case mpr
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : CompactSpace α
inst✝ : TotallyDisconnectedSpace α
x : α
U : Set α
⊢ (∃ i, (x ∈ i ∧ IsClopen i) ∧ id i ⊆ U) → U ∈ 𝓝 x
rintro ⟨V, ⟨hxV, V_op, -⟩, hUV : V ⊆ U⟩
case mpr.intro.intro.intro.intro
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : CompactSpace α
inst✝ : TotallyDisconnectedSpace α
x : α
U V : Set α
hUV : V ⊆ U
hxV : x ∈ V
V_op : IsOpen V
⊢ ∃ t, t ⊆ U ∧ IsOpen t ∧ x ∈ t
case mpr.intro.intro.intro.intro
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : CompactSpace α
inst✝ : TotallyDisconnectedSpace α
x : α
U V : Set α
hUV : V ⊆ U
hxV : x ∈ V
V_op : IsOpen V
⊢ U ∈ 𝓝 x
rw [mem_nhds_iff]
no goals
case mpr.intro.intro.intro.intro
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : CompactSpace α
inst✝ : TotallyDisconnectedSpace α
x : α
U V : Set α
hUV : V ⊆ U
hxV : x ∈ V
V_op : IsOpen V
⊢ ∃ t, t ⊆ U ∧ IsOpen t ∧ x ∈ t
exact ⟨V, hUV, V_op, hxV⟩