hasLines — Mathlib

English

Dually, if HasPoints, then there exists a HasLines structure on (P,L).

Русский

Дуально: если есть HasPoints, то существует HasLines на (P,L).

LaTeX

$$$\\text{HasLines}(P,L)$ given $\\text{HasPoints}(P,L)$$$

Lean4

/-- If a nondegenerate configuration has a unique point on any two lines, and if `|P| = |L|`,
  then there is a unique line through any two points. -/
noncomputable def hasLines [HasPoints P L] [Fintype P] [Fintype L] (h : Fintype.card P = Fintype.card L) :
    HasLines P L :=
  let this := @HasLines.hasPoints (Dual L) (Dual P) _ _ _ _ h.symm
  { ‹HasPoints P L› with
    mkLine := @fun _ _ => this.mkPoint
    mkLine_ax := @fun _ _ => this.mkPoint_ax }

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