English
A variant expressing 𝓝 f as an infimum of principal filters generated by sets of the form {g | ∀ x ∈ S, (f x, g x) ∈ V} with S ∈ 𝔖 and V from 𝓤 β.
Русский
Вариант выражения 𝓝 f как пересечения/инфинтум признакованных фильтров с множествами вида {g | ∀ x ∈ S, ...}.
LaTeX
$$$\mathcal N(f) = \bigwedge_{S∈𝔖} \bigwedge_{V∈𝓤 β} \mathcal P\{ g: ∀ x∈S, (f x, g x) ∈ V\}.$$$
Lean4
/-- A version of `UniformOnFun.hasBasis_uniformity_of_basis`
with weaker conclusion and weaker assumptions.
We make no assumptions about the set `𝔖`
but conclude only that the uniformity is equal to some indexed infimum. -/
protected theorem uniformity_eq_of_basis {ι : Sort*} {p : ι → Prop} {V : ι → Set (β × β)} (h : (𝓤 β).HasBasis p V) :
𝓤 (α →ᵤ[𝔖] β) = ⨅ s ∈ 𝔖, ⨅ (i) (_ : p i), 𝓟 (UniformOnFun.gen 𝔖 s (V i)) := by
simp_rw [iInf_uniformity, uniformity_comap, (UniformFun.hasBasis_uniformity_of_basis _ _ h).eq_biInf, comap_iInf,
comap_principal, Function.comp_apply, UniformFun.gen, Subtype.forall, UniformOnFun.gen, preimage_setOf_eq,
Prod.map_fst, Prod.map_snd, Function.comp_apply, UniformFun.toFun_ofFun, restrict_apply]
