abs_areaForm_le — Mathlib

English

If x and y are orthogonal, then the absolute value of ω(x,y) equals the product of the norms: |ω(x,y)| = ||x|| ||y||.

Русский

Если x и y ортогональны, то модуль ω(x,y) равен произведению норм: |ω(x,y)| = ||x|| ||y||.

LaTeX

$$|ω(x,y)| = ||x|| \cdot ||y|| when ⟪x,y⟫ = 0$$

Lean4

theorem abs_areaForm_le (x y : E) : |ω x y| ≤ ‖x‖ * ‖y‖ := by
  simpa [areaForm_to_volumeForm, Fin.prod_univ_succ] using o.abs_volumeForm_apply_le ![x, y]

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