not_anisotropic_iff_exists — Mathlib

English

Not every vector is mapped to 0 by Q in a straightforward sense: not anisotropic iff there exists x ≠ 0 with Q x = 0.

Русский

Не каждого вектора можно увидеть нулевым под Q; неанизотропность эквивалентна существованию x ≠ 0 с Q x = 0.

LaTeX

$$$\\neg \\mathrm{Anisotropic}(Q) \\iff \\exists x:\\!M, x \\neq 0 \\land Q(x)=0.$$$

Lean4

theorem not_anisotropic_iff_exists (Q : QuadraticMap R M N) : ¬Anisotropic Q ↔ ∃ x, x ≠ 0 ∧ Q x = 0 := by
  simp only [Anisotropic, not_forall, exists_prop, and_comm]

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