English
For 𝒮 a family of sets of α, S a subset, and V ⊆ β × β, UniformOnFun.gen 𝒮 S V equals the set of pairs (f,g) with ∀ x ∈ S, the pair (f(x), g(x)) lies in V, using the α-indexed alias 𝔖.
Русский
Для 𝒮, задание UniformOnFun.gen 𝒮 S V задаёт пары (f,g) такие, что ∀ x ∈ S, (f(x), g(x)) ∈ V, с учётом псевдонима α → β.
LaTeX
$$$$\mathrm{UniformOnFun.gen }\mathcal S S V = \{ (f,g) : (α \to^{\mathcal S} β) \times (α \to^{\mathcal S} β) \; | \; \forall x \in S, (f(x), g(x)) ∈ V \}.$$$$
Lean4
/-- Basis sets for the uniformity of `𝔖`-convergence: for `S : Set α` and `V : Set (β × β)`,
`gen 𝔖 S V` is the set of pairs `(f, g)` of functions `α →ᵤ[𝔖] β` such that
`∀ x ∈ S, (f x, g x) ∈ V`. Note that the family `𝔖 : Set (Set α)` is only used to specify which
type alias of `α → β` to use here. -/
protected def gen (𝔖) (S : Set α) (V : Set (β × β)) : Set ((α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)) :=
{uv : (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β) | ∀ x ∈ S, (toFun 𝔖 uv.1 x, toFun 𝔖 uv.2 x) ∈ V}
