not_bddAbove_range_of_wellFoundedLT

English

If f is strictly increasing, β-order well-founded and has no maximum, then the range of f is not bounded above.

Русский

Если f строго возрастание на линейном порядке без максимума, то образ f не ограничен сверху.

LaTeX

$$$\text{Let } f: β \to β,\text{ strictly increasing, and } β\text{ well-founded with no maximum. Then } \{f(x) : x\in β\} \text{ is not bounded above.}$$$

Lean4

theorem not_bddAbove_range_of_wellFoundedLT {f : β → β} [WellFoundedLT β] [NoMaxOrder β] (hf : StrictMono f) :
    ¬BddAbove (Set.range f) := by
  rintro ⟨a, ha⟩
  obtain ⟨b, hb⟩ := exists_gt a
  exact ((hf.le_apply.trans_lt (hf hb)).trans_le <| ha (Set.mem_range_self _)).false

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