not_isCofinal_iff_bddAbove — Mathlib

English

In any NoMaxOrder, ¬IsCofinal s iff BddAbove s.

Русский

В NoMaxOrder справедливо: ¬IsCofinal s эквивалентно BddAbove s.

LaTeX

$$[NoMaxOrder α] ¬IsCofinal s ↔ BddAbove s$$

Lean4

/-- In a linear order with no maximum, cofinal sets are the same as unbounded sets. -/
theorem not_isCofinal_iff_bddAbove [NoMaxOrder α] {s : Set α} : ¬IsCofinal s ↔ BddAbove s :=
  by
  use .of_not_isCofinal
  rw [not_isCofinal_iff]
  rintro ⟨x, h⟩
  obtain ⟨z, hz⟩ := exists_gt x
  exact ⟨z, fun y hy ↦ (h hy).trans_lt hz⟩

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