length_lt_card — Mathlib

English

For LTSeries s over a finite type α, the length is strictly less than the cardinality of α.

Русский

Для LTSeries s над сколь угодно конечным типом α длина строго меньше мощности α.

LaTeX

$$$\forall {\alpha} [Preorder\alpha] [Fintype\alpha] (s: LTSeries\alpha), s.length < Fintype.card\alpha$$$

Lean4

theorem length_lt_card (s : LTSeries α) : s.length < Fintype.card α :=
  by
  by_contra! h
  obtain ⟨i, j, hn, he⟩ := Fintype.exists_ne_map_eq_of_card_lt s (by rw [Fintype.card_fin]; cutsat)
  wlog hl : i < j generalizing i j
  · exact this j i hn.symm he.symm (by cutsat)
  exact absurd he (s.strictMono hl).ne

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