existsUnique_point — Mathlib

English

In a configuration with points on lines, for any two distinct lines l1 and l2 there exists a unique point p that lies on both l1 and l2.

Русский

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

LaTeX

$$$\\exists!\\, p\\; (p\\in l_1 \\land p\\in l_2)$$$

Lean4

theorem existsUnique_point [HasPoints P L] (l₁ l₂ : L) (hl : l₁ ≠ l₂) : ∃! p, p ∈ l₁ ∧ p ∈ l₂ :=
  ⟨mkPoint hl, mkPoint_ax hl, fun _ hp => (eq_or_eq hp.1 (mkPoint_ax hl).1 hp.2 (mkPoint_ax hl).2).resolve_right hl⟩

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