English
If 𝔖 is a nonempty directed family of sets and h has a basis at 0 in F, then nhds_UniformConvergenceCLM(0) has a basis indexed by (Si, p) formed from 𝔖 and h.
Русский
Если 𝔖 непустая направленная система множеств и у F есть базис в нуле, то локальная окрестность нуля в UniformConvergenceCLM имеет базис, индексируемый пары 𝔖 и базисом в F.
LaTeX
$$$\\Nhds(0)\\;\\text{HasBasis} \\;p\\;b \\Rightarrow \\Nhds(0)\\big(\\mathrm{UniformConvergenceCLM}(\\sigma,F,\\mathcal{S})\\big)\\;\\text{HasBasis} \\, (\\lambda Si. Si.1 \\in 𝔖 \\wedge p Si.2)\\; \\{f: E \\toSL[\\sigma]F \\mid \\forall x \\in Si.1, f x \\in b Si.2\\}$$$
Lean4
theorem hasBasis_nhds_zero_of_basis [TopologicalSpace F] [IsTopologicalAddGroup F] {ι : Type*} (𝔖 : Set (Set E))
(h𝔖₁ : 𝔖.Nonempty) (h𝔖₂ : DirectedOn (· ⊆ ·) 𝔖) {p : ι → Prop} {b : ι → Set F} (h : (𝓝 0 : Filter F).HasBasis p b) :
(𝓝 (0 : UniformConvergenceCLM σ F 𝔖)).HasBasis (fun Si : Set E × ι => Si.1 ∈ 𝔖 ∧ p Si.2) fun Si =>
{f : E →SL[σ] F | ∀ x ∈ Si.1, f x ∈ b Si.2} :=
by
letI : UniformSpace F := IsTopologicalAddGroup.toUniformSpace F
haveI : IsUniformAddGroup F := isUniformAddGroup_of_addCommGroup
rw [(isEmbedding_coeFn σ F 𝔖).isInducing.nhds_eq_comap]
exact (UniformOnFun.hasBasis_nhds_zero_of_basis 𝔖 h𝔖₁ h𝔖₂ h).comap DFunLike.coe
