posRootForm_posForm_anisotropic — Mathlib

English

Same content as exists_coroot_ne with the explicit existential quantification of i.

Русский

То же самое, что существует коррота i, действующего ненулево на x.

LaTeX

$$∃ i, P.coroot'In S i x ≠ 0$$

Lean4

theorem posRootForm_posForm_anisotropic : (P.posRootForm S).posForm.toQuadraticMap.Anisotropic := fun _ hx ↦
  Classical.byContradiction fun h ↦ (ne_of_lt (posRootForm_posForm_pos_of_ne_zero P S h)).symm hx

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