English
For a finite-type γ and order-embeddings e: α ≃o β, boundedness under ≤ is preserved by composition with e: IsBoundedUnder(≤) l (e ∘ u) iff IsBoundedUnder(≤) l u.
Русский
Для биективного монотонного отображения e: α ≃o β сохраняется ограниченность по ≤ при композиции: IsBoundedUnder(≤) l (e ∘ u) эквивалентно IsBoundedUnder(≤) l u.
LaTeX
$$$\text{IsBoundedUnder}(\le)\ l\ (\lambda x. e(u(x))) \ \iff\ IsBoundedUnder(\le)\ l\ u$$$
Lean4
theorem isBoundedUnder_le_sum {κ : Type*} [AddCommMonoid R] [AddLeftMono R] [AddRightMono R] {u : κ → α → R}
(s : Finset κ) : (∀ k ∈ s, f.IsBoundedUnder (· ≤ ·) (u k)) → f.IsBoundedUnder (· ≤ ·) (∑ k ∈ s, u k) := fun h ↦
isBoundedUnder_sum (fun _ _ ↦ isBoundedUnder_le_add) le_rfl s h
