instProdSeminormedAddCommGroup — Mathlib

English

There is an isometry for p = ∞: prod_isometry_ofLp_infty (same as above) holds.

Русский

Снова существует изометрия для p = ∞: prod_isometry_ofLp_infty.

LaTeX

$$$ \\text{Isometry}(\\operatorname{ofLp}_{\\infty} (\\alpha \\times \\beta)) $$$

Lean4

/-- Seminormed group instance on the product of two normed groups, using the `L^p`
norm. -/
instance instProdSeminormedAddCommGroup [SeminormedAddCommGroup α] [SeminormedAddCommGroup β] :
    SeminormedAddCommGroup (WithLp p (α × β)) where
  dist_eq x
    y := by
    rcases p.dichotomy with (rfl | h)
    · simp only [prod_dist_eq_sup, prod_norm_eq_sup, dist_eq_norm]
      rfl
    · simp only [prod_dist_eq_add (zero_lt_one.trans_le h), prod_norm_eq_add (zero_lt_one.trans_le h), dist_eq_norm]
      rfl

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