English
For a continuous map f: X → V with profinite X and S a neighborhood of diagonal in V×V, there exists a finite disjoint nonempty clopen cover of X and a coordinatewise approximation of f on each piece within S.
Русский
Для непрерывной карты f: X → V с профинитным X и S окрестность диагонали в V×V, существует конечное попарно непересекающееся клноподпространство разбиение X и аппроксимация f на каждой части внутри S.
LaTeX
$$$\exists n, D: Fin n \to Clopens X,\; (\forall i, D_i \neq \emptyset) \land \forall i,\forall y,z \in D_i, (f(y), f(z)) \in S$.$$
Lean4
/-- For any continuous function `f : X → V`, with `X` profinite, and `S` a neighbourhood of the
diagonal in `V × V`, there exists a finite cover of `X` by pairwise-disjoint nonempty clopens, on
each of which `f` varies within `S`.
-/
theorem exists_disjoint_nonempty_clopen_cover_of_mem_nhds_diagonal (hS : S ∈ nhdsSet (diagonal V)) :
∃ (n : ℕ) (D : Fin n → Clopens X),
(∀ i, D i ≠ ⊥) ∧
(∀ i, ∀ y ∈ D i, ∀ z ∈ D i, (f y, f z) ∈ S) ∧ (univ : Set X) ⊆ ⋃ i, D i ∧ Pairwise (Disjoint on D) :=
by
have : (f.prodMap f) ⁻¹' S ∈ nhdsSet (diagonal X) :=
by
rw [mem_nhdsSet_iff_forall] at hS ⊢
rintro ⟨x, y⟩ (rfl : x = y)
exact (map_continuous _).continuousAt.preimage_mem_nhds (hS _ rfl)
exact exists_finite_disjoint_nonempty_clopen_cover_of_mem_nhds_diagonal_of_profinite this
