hasBasis_nhds_zero — Mathlib

English

Specializes basis for the zero-neighborhood in CM_k(E,F) using the product basis of the input, namely an entry in nhds0 for the scalar side and von Neumann boundedness on the input side.

Русский

Особый базис ншд нуля в CM_k(E,F): используется база на входе, состоящая из Von Neumann ограниченных множеств и окрестностей нуля в F.

LaTeX

$$$\\bigl(\\mathcal{N}_0\\bigr)\\text{ HasBasis }(S, B) \\Rightarrow (\\mathcal{N}_0^{\\mathrm{CM}}) \\text{ HasBasis }\\{f:\\mathrm{MapsTo}(S) : f(S) \\subseteq B\\}\\,.$$$

Lean4

theorem hasBasis_nhds_zero :
    (𝓝 (0 : ContinuousMultilinearMap 𝕜 E F)).HasBasis
      (fun SV : Set (Π i, E i) × Set F => IsVonNBounded 𝕜 SV.1 ∧ SV.2 ∈ 𝓝 0) fun SV => {f | MapsTo f SV.1 SV.2} :=
  hasBasis_nhds_zero_of_basis (Filter.basis_sets _)

Похожие утверждения