isometry_lpMeasSubgroupToLpTrim — Mathlib

English

The trim-to-Lp map is an isometry on the norm; it preserves norms exactly for mapped elements.

Русский

Отображение обрезки сохраняет норму точно на отображённых элементах.

LaTeX

$$$\|lpMeasSubgroupToLpTrim\ F\ p\ μ hm f\| = \|f\|$$$

Lean4

theorem isometry_lpMeasSubgroupToLpTrim [hp : Fact (1 ≤ p)] (hm : m ≤ m0) :
    Isometry (lpMeasSubgroupToLpTrim F p μ hm) :=
  Isometry.of_dist_eq fun f g => by
    rw [dist_eq_norm, ← lpMeasSubgroupToLpTrim_sub, lpMeasSubgroupToLpTrim_norm_map, dist_eq_norm]

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