English
For any 𝓑 : Filter on β × β, the sets UniformFun.gen α β V with V ∈ 𝓑 form a filter basis for (α →ᵤ β) × (α →ᵤ β).
Русский
Для любого 𝓑 — фильтр на β×β, множества UniformFun.gen α β V с V ∈ 𝓑 образуют базис фильтра на (α →ᵤ β) × (α →ᵤ β).
LaTeX
$$$\\text{isBasis }(∀ V, V \\in 𝓑)\\; (UniformFun.gen α β)$$$
Lean4
/-- If `𝓕` is a filter on `β × β`, then the set of all `UniformFun.gen α β V` for
`V ∈ 𝓕` is a filter basis on `(α →ᵤ β) × (α →ᵤ β)`. 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 theorem isBasis_gen (𝓑 : Filter <| β × β) : IsBasis (fun V : Set (β × β) => V ∈ 𝓑) (UniformFun.gen α β) :=
⟨⟨univ, univ_mem⟩,
@fun U V hU hV => ⟨U ∩ V, inter_mem hU hV, fun _ huv => ⟨fun x => (huv x).left, fun x => (huv x).right⟩⟩⟩
