norm_eq — Mathlib

English

If f(0) = 0, then the norm equals the norm of the linear part.

Русский

Если f(0) = 0, то норма равна норме линейной части.

LaTeX

$$$$\|f\| = \|f.contLinear\|.$$$$

Lean4

@[simp]
theorem norm_eq (h : f 0 = 0) : ‖f‖ = ‖f.contLinear‖ :=
  calc
    ‖f‖ = max ‖f 0‖ ‖f.contLinear‖ := by rw [norm_def]
    _ = max 0 ‖f.contLinear‖ := by rw [h, norm_zero]
    _ = ‖f.contLinear‖ := max_eq_right (norm_nonneg _)

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