α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : CompactSpace α
inst✝ : TotallyDisconnectedSpace α
⊢ ∀ (a : α) (u : Set α), a ∈ u → IsOpen u → ∃ v, (v ∈ fun U => IsOpen U ∧ IsClosed U) ∧ a ∈ v ∧ v ⊆ u
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : CompactSpace α
inst✝ : TotallyDisconnectedSpace α
⊢ IsTopologicalBasis {s | IsClopen s}
apply isTopologicalBasis_of_open_of_nhds fun U (hU : IsClopen U) => hU.1
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : CompactSpace α
inst✝ : TotallyDisconnectedSpace α
x : α
U : Set α
hxU : x ∈ U
U_op : IsOpen U
⊢ ∃ v, (v ∈ fun U => IsOpen U ∧ IsClosed U) ∧ x ∈ v ∧ v ⊆ U
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : CompactSpace α
inst✝ : TotallyDisconnectedSpace α
⊢ ∀ (a : α) (u : Set α), a ∈ u → IsOpen u → ∃ v, (v ∈ fun U => IsOpen U ∧ IsClosed U) ∧ a ∈ v ∧ v ⊆ u
intro x U hxU U_op
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : CompactSpace α
inst✝ : TotallyDisconnectedSpace α
x : α
U : Set α
hxU : x ∈ U
U_op : IsOpen U
this : U ∈ 𝓝 x
⊢ ∃ v, (v ∈ fun U => IsOpen U ∧ IsClosed U) ∧ x ∈ v ∧ v ⊆ U
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : CompactSpace α
inst✝ : TotallyDisconnectedSpace α
x : α
U : Set α
hxU : x ∈ U
U_op : IsOpen U
⊢ ∃ v, (v ∈ fun U => IsOpen U ∧ IsClosed U) ∧ x ∈ v ∧ v ⊆ U
have : U ∈ 𝓝 x := IsOpen.mem_nhds U_op hxU
case intro.intro.intro
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : CompactSpace α
inst✝ : TotallyDisconnectedSpace α
x : α
U : Set α
hxU : x ∈ U
U_op : IsOpen U
this : U ∈ 𝓝 x
V : Set α
hVU : V ⊆ U
hxV : x ∈ V
hV : IsClopen V
⊢ ∃ v, (v ∈ fun U => IsOpen U ∧ IsClosed U) ∧ x ∈ v ∧ v ⊆ U
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : CompactSpace α
inst✝ : TotallyDisconnectedSpace α
x : α
U : Set α
hxU : x ∈ U
U_op : IsOpen U
this : U ∈ 𝓝 x
⊢ ∃ v, (v ∈ fun U => IsOpen U ∧ IsClosed U) ∧ x ∈ v ∧ v ⊆ U
rcases (nhds_basis_clopen x).mem_iff.mp this with ⟨V, ⟨hxV, hV⟩, hVU : V ⊆ U⟩
case intro.intro.intro
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : CompactSpace α
inst✝ : TotallyDisconnectedSpace α
x : α
U : Set α
hxU : x ∈ U
U_op : IsOpen U
this : U ∈ 𝓝 x
V : Set α
hVU : V ⊆ U
hxV : x ∈ V
hV : IsClopen V
⊢ (V ∈ fun U => IsOpen U ∧ IsClosed U) ∧ x ∈ V ∧ V ⊆ U
case intro.intro.intro
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : CompactSpace α
inst✝ : TotallyDisconnectedSpace α
x : α
U : Set α
hxU : x ∈ U
U_op : IsOpen U
this : U ∈ 𝓝 x
V : Set α
hVU : V ⊆ U
hxV : x ∈ V
hV : IsClopen V
⊢ ∃ v, (v ∈ fun U => IsOpen U ∧ IsClosed U) ∧ x ∈ v ∧ v ⊆ U
use V
no goals
case intro.intro.intro
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : CompactSpace α
inst✝ : TotallyDisconnectedSpace α
x : α
U : Set α
hxU : x ∈ U
U_op : IsOpen U
this : U ∈ 𝓝 x
V : Set α
hVU : V ⊆ U
hxV : x ∈ V
hV : IsClopen V
⊢ (V ∈ fun U => IsOpen U ∧ IsClosed U) ∧ x ∈ V ∧ V ⊆ U
tauto