English
The basis def for the uniform convergence on (α →ᵤ β) × (α →ᵤ β) given a filter 𝓕 on β × β.
Русский
Базис равномерной сходимости для (α →ᵤ β) × (α →ᵤ β) задаётся через 𝓕 на β×β.
LaTeX
$$$\\text{UniformFun}.basis\\; α\\; β\\; 𝓕 : \\text{FilterBasis}((α →ᵤ β) × (α →ᵤ β))$$$
Lean4
/-- For `𝓕 : Filter (β × β)`, this is the set of all `UniformFun.gen α β V` for
`V ∈ 𝓕` as a bundled `FilterBasis` over `(α →ᵤ β) × (α →ᵤ β)`. This will only be applied to
`𝓕 = 𝓤 β` when `β` is equipped with a `UniformSpace` structure, but it is useful to define it for
any filter in order to be able to state that it has a lower adjoint
(see `UniformFun.gc`). -/
protected def basis (𝓕 : Filter <| β × β) : FilterBasis ((α →ᵤ β) × (α →ᵤ β)) :=
(UniformFun.isBasis_gen α β 𝓕).filterBasis
