English
A locally compact Hausdorff totally disconnected space has a basis consisting of clopen sets.
Русский
Локально компактное хаусдорфово полностью несвязное пространство имеет базис из клипповых множеств.
LaTeX
$$$\\text{LocallyCompactSpace } H \\land \\text{T2Space } H \\land \\text{TotallyDisconnectedSpace } H \\Rightarrow \\text{IsTopologicalBasis }\\{s:\\text{Set }H \\mid IsClopen s\\}$.$$
Lean4
theorem nhds_basis_clopen (x : X) : (𝓝 x).HasBasis (fun s : Set X => x ∈ s ∧ IsClopen s) id :=
⟨fun U => by
constructor
· have hx : connectedComponent x = { x } := totallyDisconnectedSpace_iff_connectedComponent_singleton.mp ‹_› x
rw [connectedComponent_eq_iInter_isClopen] at hx
intro hU
let N := { s // IsClopen s ∧ x ∈ s }
rsuffices ⟨⟨s, hs, hs'⟩, hs''⟩ : ∃ s : N, s.val ⊆ U
· exact ⟨s, ⟨hs', hs⟩, hs''⟩
haveI : Nonempty N := ⟨⟨univ, isClopen_univ, mem_univ x⟩⟩
have hNcl : ∀ s : N, IsClosed s.val := fun s => s.property.1.1
have hdir : Directed Superset fun s : N => s.val :=
by
rintro ⟨s, hs, hxs⟩ ⟨t, ht, hxt⟩
exact ⟨⟨s ∩ t, hs.inter ht, ⟨hxs, hxt⟩⟩, inter_subset_left, inter_subset_right⟩
have h_nhds : ∀ y ∈ ⋂ s : N, s.val, U ∈ 𝓝 y := fun y y_in =>
by
rw [hx, mem_singleton_iff] at y_in
rwa [y_in]
exact exists_subset_nhds_of_compactSpace hdir hNcl h_nhds
· rintro ⟨V, ⟨hxV, -, V_op⟩, hUV : V ⊆ U⟩
rw [mem_nhds_iff]
exact ⟨V, hUV, V_op, hxV⟩⟩
