English
If 𝔖 is nonempty and directed and 𝓑 is a basis for 𝓤 β, then UniformOnFun.gen 𝔖 S V yields a basis for the product uniformity on (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β).
Русский
Если 𝔖 непусто и направлено, и 𝓑 — база для 𝓤 β, то UniformOnFun.gen 𝔖 S V образует базис для произведения равномерностей.
LaTeX
$$$\text{If } 𝔖, 𝓑 \text{ satisfy the assumptions, then } (\mathcal U(α→ᵤ[𝔖]β))_{×} (α→ᵤ[𝔖]β) \text{ has basis } UniformOnFun.gen 𝔖 S V.$$$
Lean4
/-- If `𝔖 : Set (Set α)` is nonempty and directed and `𝓑` is a filter basis of `𝓤 β`, then the
uniformity of `α →ᵤ[𝔖] β` admits the family `{(f, g) | ∀ x ∈ S, (f x, g x) ∈ V}` for `S ∈ 𝔖` and
`V ∈ 𝓑` as a filter basis. -/
protected theorem hasBasis_uniformity_of_basis (h : 𝔖.Nonempty) (h' : DirectedOn (· ⊆ ·) 𝔖) {p : ι → Prop}
{s : ι → Set (β × β)} (hb : HasBasis (𝓤 β) p s) :
(𝓤 (α →ᵤ[𝔖] β)).HasBasis (fun Si : Set α × ι => Si.1 ∈ 𝔖 ∧ p Si.2) fun Si => UniformOnFun.gen 𝔖 Si.1 (s Si.2) :=
by
simp only [iInf_uniformity]
exact
hasBasis_biInf_of_directed h (fun S => UniformOnFun.gen 𝔖 S ∘ s) _
(fun S _hS => UniformOnFun.hasBasis_uniformity_of_basis_aux₁ α β 𝔖 hb S)
(UniformOnFun.hasBasis_uniformity_of_basis_aux₂ α β 𝔖 h' hb)
