one_lt_order — Mathlib

English

In a finite projective plane, the order is strictly greater than 1.

Русский

В конечной проективной плоскости порядок строго больше единицы.

LaTeX

$$$ 1 < \operatorname{order} P L $$$

Lean4

theorem one_lt_order [Finite P] [Finite L] : 1 < order P L :=
  by
  obtain ⟨p₁, p₂, p₃, l₁, l₂, l₃, -, -, h₂₁, h₂₂, h₂₃, h₃₁, h₃₂, h₃₃⟩ := @exists_config P L _ _
  cases nonempty_fintype { p : P // p ∈ l₂ }
  rw [← add_lt_add_iff_right 1, ← pointCount_eq _ l₂, pointCount, Nat.card_eq_fintype_card, Fintype.two_lt_card_iff]
  simp_rw [Ne, Subtype.ext_iff]
  have h := mkPoint_ax (P := P) (L := L) fun h => h₂₁ ((congr_arg (p₂ ∈ ·) h).mpr h₂₂)
  exact
    ⟨⟨mkPoint _, h.2⟩, ⟨p₂, h₂₂⟩, ⟨p₃, h₃₂⟩, ne_of_mem_of_not_mem h.1 h₂₁, ne_of_mem_of_not_mem h.1 h₃₁,
      ne_of_mem_of_not_mem h₂₃ h₃₃⟩

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