English
Basis sets for the uniformity of uniform convergence: gen α β V is the set of pairs (f,g) of functions α →ᵤ β such that ∀ x, (f x, g x) ∈ V.
Русский
Базисные множества для равномерности сходимости: gen α β V — это множество пар (f,g) функций α →ᵤ β such that ∀ x, (f x, g x) ∈ V.
LaTeX
$$$\\mathrm{UniformFun}.gen\\;α\\;β\\;V = \\{ uv = (f,g) : (α \\toᵤ β) \\times (α \\toᵤ β) \\mid \\forall x, (toFun f x, toFun g x) \\in V \\}$$$
Lean4
/-- Basis sets for the uniformity of uniform convergence: `gen α β V` is the set of pairs `(f, g)`
of functions `α →ᵤ β` such that `∀ x, (f x, g x) ∈ V`. -/
protected def gen (V : Set (β × β)) : Set ((α →ᵤ β) × (α →ᵤ β)) :=
{uv : (α →ᵤ β) × (α →ᵤ β) | ∀ x, (toFun uv.1 x, toFun uv.2 x) ∈ V}
