abs_areaForm_of_orthogonal — Mathlib

English

If ⟪x,y⟫ = 0 then |ω(x,y)| = ||x|| ||y||.

Русский

Если ⟪x,y⟫ = 0, то |ω(x,y)| = ||x|| ||y||.

LaTeX

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

Lean4

theorem abs_areaForm_of_orthogonal {x y : E} (h : ⟪x, y⟫ = 0) : |ω x y| = ‖x‖ * ‖y‖ :=
  by
  rw [o.areaForm_to_volumeForm, o.abs_volumeForm_apply_of_pairwise_orthogonal]
  · simp [Fin.prod_univ_succ]
  intro i j hij
  fin_cases i <;> fin_cases j
  · simp_all
  · simpa using h
  · simpa [real_inner_comm] using h
  · simp_all

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