English
If f is strictly monotone from a NoMaxOrder domain to a SuccArchimedean codomain, then its range is not bounded above.
Русский
Если f строго монотонна и область не имеет верхней грани, а кодом является SuccArchimedean, то образ функции не ограничен сверху.
LaTeX
$$$ \forall f,\ (\text{strictly monotone})\land (NoMaxOrder\ domain)\Rightarrow \lnot \mathrm{BddAbove}(\mathrm{range}(f)).$$$
Lean4
theorem not_bddAbove_range_of_isSuccArchimedean [NoMaxOrder α] [SuccOrder β] [IsSuccArchimedean β] (hf : StrictMono f) :
¬BddAbove (Set.range f) := by
rintro ⟨m, hm⟩
have hm' : ∀ a, f a ≤ m := fun a ↦ hm <| Set.mem_range_self _
obtain ⟨a₀⟩ := ‹Nonempty α›
suffices ∀ b, f a₀ ≤ b → ∃ a, b < f a
by
obtain ⟨a, ha⟩ : ∃ a, m < f a := this m (hm' a₀)
exact ha.not_ge (hm' a)
have h : ∀ a, ∃ a', f a < f a' := fun a ↦ (exists_gt a).imp (fun a' h ↦ hf h)
apply Succ.rec
· exact h a₀
rintro b _ ⟨a, hba⟩
exact (h a).imp (fun a' ↦ (succ_le_of_lt hba).trans_lt)
