Nondegenerate — Mathlib

English

If a configuration (P,L) is nondegenerate, then the dual configuration (Dual L, Dual P) is also nondegenerate.

Русский

Если конфигурация (P,L) непредназначена (невырожденная), то дуальная конфигурация (Dual L, Dual P) тоже непредназначена.

LaTeX

$$$\\text{Nondegenerate}(Dual\\,L, Dual\\,P)$ whenever $\\text{Nondegenerate}(P,L)$$$

Lean4

instance Nondegenerate [Nondegenerate P L] : Nondegenerate (Dual L) (Dual P)
    where
  exists_point := @exists_line P L _ _
  exists_line := @exists_point P L _ _
  eq_or_eq := @fun l₁ l₂ p₁ p₂ h₁ h₂ h₃ h₄ => (@eq_or_eq P L _ _ p₁ p₂ l₁ l₂ h₁ h₃ h₂ h₄).symm

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