lpBCF — Mathlib

English

The norm on lp E p corresponds under the lpPiLp equivalence to the corresponding norm on PiLp p E.

Русский

Норма на lp E p соответствует под эквивалентностью lpPiLp соответствующей норме на PiLp p E.

LaTeX

$$$\|\mathrm{lpPiLp} f\| = \|f\|$$$

Lean4

/-- The canonical map between `lp (fun _ : α ↦ E) ∞` and `α →ᵇ E` as an `AddEquiv`. -/
noncomputable def lpBCF : lp (fun _ : α ↦ E) ∞ ≃+ (α →ᵇ E)
    where
  toFun f := ofNormedAddCommGroupDiscrete f ‖f‖ <| le_ciSup (memℓp_infty_iff.mp f.prop)
  invFun f := ⟨⇑f, f.bddAbove_range_norm_comp⟩
  map_add' _f _g := rfl

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