English
For linear orders with a least element, coboundedness of a function under ≤ with respect to an infimum folding corresponds to coboundedness of its components.
Русский
Для линейного порядка с наименьшим элементом,coboundedness при ≤ и инфиморе сводит к coboundedness компонент.
LaTeX
$$$\operatorname{isCoboundedUnder}(\le, F)\big(\lambda a. f_i(a)\big) \Rightarrow \text{(inf over i)}$$
Lean4
theorem isBoundedUnder_le_comp_iff [Nonempty β] [LinearOrder β] [Preorder γ] [NoMaxOrder γ] {g : β → γ} {f : α → β}
{l : Filter α} (hg : Monotone g) (hg' : Tendsto g atTop atTop) :
IsBoundedUnder (· ≤ ·) l (g ∘ f) ↔ IsBoundedUnder (· ≤ ·) l f :=
by
refine ⟨?_, fun h => h.isBoundedUnder (α := β) hg⟩
rintro ⟨c, hc⟩; rw [eventually_map] at hc
obtain ⟨b, hb⟩ : ∃ b, ∀ a ≥ b, c < g a := eventually_atTop.1 (hg'.eventually_gt_atTop c)
exact ⟨b, hc.mono fun x hx => not_lt.1 fun h => (hb _ h.le).not_ge hx⟩
