English
Analogous auxiliary statement for the second basis construction; the directedness together with HasBasis for 𝓑 yields a uniformity basis on the space of 𝔖-convergent maps.
Русский
Аналогично для второго базиса: направленность и HasBasis для 𝓑 задают базис равномерности на пространстве 𝔖-сходимых отображений.
LaTeX
$$$\text{Under } h: \text{DirectedOn} (· ⊆ ·) 𝔖 \text{ and } hb,\; (\text{uniformity on } α→ᵤ[𝔖]β) \text{ has a basis induced similarly.}$$$
Lean4
protected theorem hasBasis_uniformity_of_basis_aux₂ (h : DirectedOn (· ⊆ ·) 𝔖) {p : ι → Prop} {s : ι → Set (β × β)}
(hb : HasBasis (𝓤 β) p s) :
DirectedOn ((fun s : Set α => (UniformFun.uniformSpace s β).comap (s.restrict : (α →ᵤ β) → s →ᵤ β)) ⁻¹'o GE.ge) 𝔖 :=
h.mono fun _ _ hst =>
((UniformOnFun.hasBasis_uniformity_of_basis_aux₁ α β 𝔖 hb _).le_basis_iff
(UniformOnFun.hasBasis_uniformity_of_basis_aux₁ α β 𝔖 hb _)).mpr
fun V hV => ⟨V, hV, UniformOnFun.gen_mono hst subset_rfl⟩
