English
Let β be a preorder which is directed under ≤. If f: α → β is bounded above along cofiniteness, then the range of f is bounded above.
Русский
Пусть β упорядочено и направлено по отношению ≤. Если отображение f: α → β ограничено сверху по cofiniteness, то множество значений range f ограничено сверху.
LaTeX
$$$\forall \alpha \beta [\text{Preorder } \beta] [\text{IsDirected } \beta (\le)]\, {f: \alpha \to \beta},\ (\operatorname{IsBoundedUnder}(\le)\ \text{cofinite } f) \Rightarrow \operatorname{BddAbove}(\operatorname{range} f).$$$$
Lean4
theorem bddAbove_range_of_cofinite [Preorder β] [IsDirected β (· ≤ ·)] {f : α → β}
(hf : IsBoundedUnder (· ≤ ·) cofinite f) : BddAbove (range f) :=
by
rcases hf with ⟨b, hb⟩
haveI : Nonempty β := ⟨b⟩
rw [← image_univ, ← union_compl_self {x | f x ≤ b}, image_union, bddAbove_union]
exact ⟨⟨b, forall_mem_image.2 fun x => id⟩, (hb.image f).bddAbove⟩
