anisotropic — Mathlib

English

If a quadratic map Q is positive definite, then Q is anisotropic; i.e., every nonzero x satisfies Q(x) ≠ 0.

Русский

Если квадратичная карта Q является положительно определённой, то она анизотропна; то есть для любого ненулевого вектора x верно Q(x) ≠ 0.

LaTeX

$$$\operatorname{PosDef}(Q) \Rightarrow \operatorname{Anisotropic}(Q)$$$

Lean4

theorem anisotropic {Q : QuadraticMap R₂ M N} (hQ : Q.PosDef) : Q.Anisotropic := fun x hQx =>
  by_contradiction fun hx =>
    lt_irrefl (0 : N) <| by
      have := hQ _ hx
      rw [hQx] at this
      exact this

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