English
For a continuous f: X → V with profinite X and S ⊆ V×V a neighborhood of the diagonal, there exist n, a map g : X → Fin n and h : Fin n → V with f(x) ≈ h(g(x)) within S for all x.
Русский
Для непрерывной карты f: X → V с профинитным X и S, окрестность диагонали в V×V, существуют n, отображение g: X → Fin n и h: Fin n → V так, что для всех x верно (f(x), h(g(x))) ∈ S.
LaTeX
$$$\exists n, g: X \to \mathrm{Fin}_n, h: \mathrm{Fin}_n \to V,\; \text{Continuous}(g) \,\land\, \forall x, (f(x), h(g(x))) \in S.$$$
Lean4
/-- For any continuous function `f : X → V`, with `X` profinite, and `S` a neighbourhood of the
diagonal in `V × V`, the function `f` can be `S`-approximated by a function factoring through
`Fin n`, for some `n`. -/
theorem exists_finite_approximation_of_mem_nhds_diagonal (hS : S ∈ nhdsSet (diagonal V)) :
∃ (n : ℕ) (g : X → Fin n) (h : Fin n → V), Continuous g ∧ ∀ x, (f x, h (g x)) ∈ S :=
by
obtain ⟨n, E, hEne, hES, hEuniv, hEdis⟩ := exists_disjoint_nonempty_clopen_cover_of_mem_nhds_diagonal f hS
have h_uniq (x) : ∃! i, x ∈ E i :=
by
refine
match mem_iUnion.mp (hEuniv <| mem_univ x) with
| ⟨i, hi⟩ => ⟨i, hi, fun j hj ↦ hEdis.eq ?_⟩
simpa [← Clopens.coe_disjoint, not_disjoint_iff] using ⟨x, hj, hi⟩
choose g hg hg' using h_uniq
have h_ex (i) : ∃ x, x ∈ E i := by simpa [← SetLike.coe_set_eq, ← nonempty_iff_ne_empty] using hEne i
choose r hr using h_ex
refine ⟨n, g, f ∘ r, continuous_discrete_rng.mpr fun j ↦ ?_, fun x ↦ (hES _) _ (hg _) _ (hr _)⟩
convert (E j).isOpen
exact Set.ext fun x ↦ ⟨fun hj ↦ hj ▸ hg x, fun hx ↦ (hg' _ _ hx).symm⟩
