norm_eq_max_natAbs — Mathlib

English

The norm of the symmetric two-entry vector is symmetric under swapping the entries.

Русский

Норма симметрична при перестановке двух компонент вектора.

LaTeX

$$‖![x,y]‖ = ‖![y,x]‖$$

Lean4

theorem norm_eq_max_natAbs (x : Fin 2 → ℤ) : ‖x‖ = max (x 0).natAbs (x 1).natAbs :=
  by
  rw [← coe_nnnorm, ← NNReal.coe_natCast, NNReal.coe_inj, Nat.cast_max]
  refine eq_of_forall_ge_iff fun c ↦ ?_
  simp only [pi_nnnorm_le_iff, Fin.forall_fin_two, max_le_iff, NNReal.natCast_natAbs]

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