idemSnd — Mathlib

English

There is a linear isometric equivalence between WithLp p (α×β) and α×β given by the canonical projection map; i.e., prodEquivₗᵢ p is an isometric isomorphism.

Русский

Существует линейное изометрическое эквалентное отображение между WithLp p (α×β) и α×β, заданное каноническим отображением проекции.

LaTeX

$$$WithLp\ p\ (\alpha \times \beta) \cong_{\text{isom}} \alpha \times \beta$$$

Lean4

/-- Projection on `WithLp p (α × β)` with range `β` and kernel `α` -/
def idemSnd : AddMonoid.End (WithLp p (α × β)) :=
  (AddMonoidHom.inr α β).comp (AddMonoidHom.snd α β)

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