unitization_addEquiv_prod — Mathlib

English

The natural map between WithLp 1 (Unitization 𝕜 A) and WithLp 1 (𝕜 × A) is an additive equivalence.

Русский

Естественное отображение между WithLp 1 (Unitization 𝕜 A) и WithLp 1 (𝕜 × A) является добавочнымэквивалентом.

LaTeX

$$$$\\text{unitization\_addEquiv\_prod} : WithLp 1 (Unitization 𝕜 A) \\simeq_+ WithLp 1 (𝕜 \\times A).$$$$

Lean4

/-- The natural map between `Unitization 𝕜 A` and `𝕜 × A`, transferred to their `WithLp 1`
synonyms. -/
noncomputable def unitization_addEquiv_prod : WithLp 1 (Unitization 𝕜 A) ≃+ WithLp 1 (𝕜 × A) :=
  (WithLp.linearEquiv 1 𝕜 (Unitization 𝕜 A)).toAddEquiv.trans <|
    (addEquiv 𝕜 A).trans (WithLp.linearEquiv 1 𝕜 (𝕜 × A)).symm.toAddEquiv

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