hasBasis_nhds_zero_of_basis — Mathlib

English

The zero neighborhood basis in the space of continuous alternating maps is generated by finite von Neumann-type boundedness constraints on the domain together with a neighborhood basis in the codomain.

Русский

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

LaTeX

$$$\\mathcal{N}_0 =\\{ \\text{maps to bounded domain with basis near }0\\}$$$

Lean4

theorem hasBasis_nhds_zero_of_basis {ι' : Type*} {p : ι' → Prop} {b : ι' → Set F} (h : (𝓝 (0 : F)).HasBasis p b) :
    (𝓝 (0 : E [⋀^ι]→L[𝕜] F)).HasBasis (fun Si : Set (ι → E) × ι' => IsVonNBounded 𝕜 Si.1 ∧ p Si.2) fun Si =>
      {f | MapsTo f Si.1 (b Si.2)} :=
  by
  rw [nhds_induced]
  exact (ContinuousMultilinearMap.hasBasis_nhds_zero_of_basis h).comap _

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