English
In an ordered group, applying inversion to a function u preserves a form of boundedness along a filter: IsBoundedUnder(≥) along l of u⁻¹ is equivalent to IsBoundedUnder(≤) along l of u.
Русский
В упорядоченной группе сохранение ограниченности при взятии обратного элемента: IsBoundedUnder(≥) вдоль фильтра l от u⁻¹ эквивалентно IsBoundedUnder(≤) вдоль l от u.
LaTeX
$$$(\operatorname{IsBoundedUnder}(\ge)\ l\ (u\, \cdot) ) \iff (\operatorname{IsBoundedUnder}(\le)\ l\ u)$$$
Lean4
@[to_additive (attr := simp)]
theorem isBoundedUnder_ge_inv [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] {l : Filter β} {u : β → α} :
(IsBoundedUnder (· ≥ ·) l fun x => (u x)⁻¹) ↔ IsBoundedUnder (· ≤ ·) l u :=
(OrderIso.inv α).isBoundedUnder_le_comp
