English
In an additive group with a linear order, the boundedness of |u| in the ≤-sense is equivalent to u being bounded above and below along the filter.
Русский
В/additive-группе с линейным порядком, ограниченность |u| по отношению ≤ эквивалентна тому, что u ограничено сверху и снизу вдоль фильтра.
LaTeX
$$$\operatorname{IsBoundedUnder}(\le, l)(|u|) \iff \bigl(\operatorname{IsBoundedUnder}(\le, l)u \land \operatorname{IsBoundedUnder}(\ge, l)u\bigr)$$$
Lean4
theorem isBoundedUnder_le_abs [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] {f : Filter β} {u : β → α} :
(f.IsBoundedUnder (· ≤ ·) fun a => |u a|) ↔ f.IsBoundedUnder (· ≤ ·) u ∧ f.IsBoundedUnder (· ≥ ·) u :=
isBoundedUnder_le_sup.trans <| and_congr Iff.rfl isBoundedUnder_le_neg
