of_forall_not_lt_lt — Mathlib

English

If a linear order α contains no triple x < y < z, then α is finite.

Русский

Если линейный порядок α не содержит тройку x<y<z, то α конечен.

LaTeX

$$$ (\forall x,y,z\in α,\ x

Lean4

/-- If a linear order does not contain any triple of elements `x < y < z`, then this type
is finite. -/
theorem of_forall_not_lt_lt (h : ∀ ⦃x y z : α⦄, x < y → y < z → False) : Finite α :=
  by
  nontriviality α
  rcases exists_pair_ne α with ⟨x, y, hne⟩
  refine @Finite.of_fintype α ⟨{ x, y }, fun z => ?_⟩
  simpa [hne] using eq_or_eq_or_eq_of_forall_not_lt_lt h z x y

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