English
If s is PartiallyWellOrderedOn r and f: ℕ → α is strictly r-decreasing along indices, then the preimage s.preimage f is bounded above.
Русский
Если s частично хорошо упорядочено по r и f: ℕ → α строго убывает по индексам, то прообраз s.preimage f ограничен сверху.
LaTeX
$$({s} .PartiallyWellOrderedOn r) \rightarrow (\forall m n : ℕ, m < n \rightarrow ¬ r (f m) (f n)) \rightarrow BddAbove (s.preimage f)$$
Lean4
theorem bddAbove_preimage {s : Set α} (hs : s.PartiallyWellOrderedOn r) {f : ℕ → α}
(hf : ∀ m n : ℕ, m < n → ¬r (f m) (f n)) : BddAbove (s.preimage f) :=
by
contrapose! hf
rw [not_bddAbove_iff] at hf
obtain ⟨φ, hφm, hφs⟩ :=
Nat.exists_strictMono_subsequence fun n ↦ (hf n).casesOn fun m h ↦ h.casesOn fun hs hmn ↦ Exists.intro m ⟨hmn, hs⟩
rw [partiallyWellOrderedOn_iff_exists_lt] at hs
obtain ⟨m, n, hmn, hr⟩ := hs (fun n ↦ f (φ n)) hφs
use (φ m), (φ n)
exact ⟨hφm hmn, hr⟩
