English
A weaker form of the basis lemma stating that even without 𝔖 assumptions one can express 𝓤(α→ᵤ[𝔖]β) as an indexed infimum of principal entourages built from UniformOnFun.gen.
Русский
Слабая форма базы: даже без предположений про 𝔖 можно выразить 𝓤(α→ᵤ[𝔖]β) как индексованный инфимум над окружениями, порождаемых UniformOnFun.gen.
LaTeX
$$$\mathcal U(α→ᵤ[𝔖]β) = ⨅ s ∈ 𝔖, ⨅ i (⨅ H ∈ 𝓟, 𝓟 (UniformOnFun.gen 𝔖 s (V i))).$$$
Lean4
/-- A version of `UniformOnFun.hasBasis_nhds_of_basis`
with weaker conclusion and weaker assumptions.
We make no assumptions about the set `𝔖`
but conclude only that the neighbourhoods filter is equal to some indexed infimum. -/
protected theorem nhds_eq_of_basis {ι : Sort*} {p : ι → Prop} {V : ι → Set (β × β)} (h : (𝓤 β).HasBasis p V)
(f : α →ᵤ[𝔖] β) : 𝓝 f = ⨅ s ∈ 𝔖, ⨅ (i) (_ : p i), 𝓟 {g | ∀ x ∈ s, (toFun 𝔖 f x, toFun 𝔖 g x) ∈ V i} := by
simp_rw [nhds_eq_comap_uniformity, UniformOnFun.uniformity_eq_of_basis _ _ h, comap_iInf, comap_principal,
UniformOnFun.gen, preimage_setOf_eq]
