finite_of_forall_not_lt_lt — Mathlib

English

If a subset s of a linear order α contains no triple x<y<z with x,y,z in s, then s is finite.

Русский

Если подмножество s линейного порядка α не содержит тройку x<y<z с x,y,z∈s, то s конечно.

LaTeX

$$$ \forall x\in s,\forall y\in s,\forall z\in s, x

Lean4

/-- If a set `s` does not contain any triple of elements `x < y < z`, then `s` is finite. -/
theorem finite_of_forall_not_lt_lt (h : ∀ x ∈ s, ∀ y ∈ s, ∀ z ∈ s, x < y → y < z → False) : Set.Finite s :=
  @Set.toFinite _ s <| Finite.of_forall_not_lt_lt <| by simpa only [SetCoe.forall'] using h

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