volumeForm_apply_le — Mathlib

English

The volume form value on a vector is bounded above by the product of the norms of the components.

Русский

Значение объемной формы на наборе векторов не превосходит произведение норм компонент.

LaTeX

$$$$ o.volumeForm(v) \le \prod_{i=1}^n \|v_i\|. $$$$

Lean4

theorem volumeForm_apply_le (v : Fin n → E) : o.volumeForm v ≤ ∏ i : Fin n, ‖v i‖ :=
  (le_abs_self _).trans (o.abs_volumeForm_apply_le v)

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