existsUnique_line — Mathlib

English

In a configuration with HasLines, for any two distinct points p1 and p2 there exists a unique line l with p1 ∈ l and p2 ∈ l.

Русский

В конфигурации HasLines через две различные точки существует единственная прямая, содержащая обе точки.

LaTeX

$$$\\exists!\\, l\\; (p_1\\in l \\land p_2\\in l)$$$

Lean4

theorem existsUnique_line [HasLines P L] (p₁ p₂ : P) (hp : p₁ ≠ p₂) : ∃! l : L, p₁ ∈ l ∧ p₂ ∈ l :=
  HasPoints.existsUnique_point (Dual L) (Dual P) p₁ p₂ hp

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