Neighborhoods of profinite

Stream: Is there code for X?

[Andrew Yang]

Do we have the fact that every neighborhood in a profinite space can be shrunk into a clopen neighborhood? Concretely I'm looking for the following:

import Mathlib.Topology.Algebra.OpenSubgroup

open Topology

variable {α} [TopologicalSpace α] [CompactSpace α] [T2Space α] [TotallyDisconnectedSpace α]

theorem Profinite.exists_isClopen_of_mem_nhds {x : α} {U : Set α} (hU : U ∈ 𝓝 x) :
    ∃ K, IsClopen K ∧ x ∈ K ∧ K ⊆ U := sorry

@[to_additive]
theorem Profinite.exists_subgroup_subset
    [CommGroup α] [TopologicalGroup α] {U : Set α} (hU : U ∈ 𝓝 1) :
    ∃ G : Subgroup α, IsOpen (X := α) G ∧ (G : Set α) ⊆ U := by
  obtain ⟨K, hK, hxK, hKU⟩ := Profinite.exists_isClopen_of_mem_nhds hU
  obtain ⟨⟨G, hG⟩, hG'⟩ := TopologicalGroup.exist_openSubgroup_sub_clopen_nhd_of_one hK hxK
  exact ⟨G, hG, hG'.trans hKU⟩

theorem Profinite.exists_ideal_subset
    [Ring α] [TopologicalRing α] {U : Set α} (hU : U ∈ 𝓝 0) :
    ∃ I : Ideal α, IsOpen (X := α) I ∧ (I : Set α) ⊆ U := sorry

[Matt Diamond]

You can solve Profinite.exists_isClopen_of_mem_nhds with isTopologicalBasis_isClopen.mem_nhds_iff.mp hU

docs#isTopologicalBasis_isClopen
docs#TopologicalSpace.IsTopologicalBasis.mem_nhds_iff

[Andrew Yang]

Yes that’s exactly what I want. Thanks!