hasBasis_nhds_zero — Mathlib

English

There exists a standardized HasBasis description for the zero neighborhood in the space of continuous alternating maps, built from VonNBounded sets and the codomain's neighborhoods.

Русский

Существет стандартное описание HasBasis для нулевого окрестности в пространстве непрерывных чередующихся отображений, составляемое из VonNBounded множеств и окрестностей кодома.

LaTeX

$$$\\text{HasBasis}(\\mathcal{N}_0, (\\cdot), (\\cdot))$$$

Lean4

theorem hasBasis_nhds_zero :
    (𝓝 (0 : E [⋀^ι]→L[𝕜] F)).HasBasis (fun SV : Set (ι → E) × 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 _)

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