opNorm_flip — Mathlib

English

Flip preserves the operator norm: ||f.flip|| = ||f|| for any bilinear operator f.

Русский

Операция flip сохраняет операторную норму: ||f.flip|| = ||f|| для любой билинейной операции f.

LaTeX

$$$$ \|f.flip\| = \|f\| $$$$

Lean4

@[simp]
theorem opNorm_flip (f : E →SL[σ₁₃] F →SL[σ₂₃] G) : ‖f.flip‖ = ‖f‖ :=
  le_antisymm (by simpa only [flip_flip] using le_norm_flip f.flip) (le_norm_flip f)

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