isBoundedUnder_le_inv — Mathlib

English

For CommGroup α with partial order and IsOrderedMonoid structure, there is an equivalence between IsBoundedUnder(≤) of the inverse of u and IsBoundedUnder(≥) of u.

Русский

Для комм-группы с частичным порядком и структурой IsOrderedMonoid существует эквивалентность между IsBoundedUnder(≤) инверсии u и IsBoundedUnder(≥) u.

LaTeX

$$$(OrderIso.inv\ α).isBoundedUnder_ge_comp$$$

Lean4

@[to_additive (attr := simp)]
theorem isBoundedUnder_le_inv [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] {l : Filter β} {u : β → α} :
    (IsBoundedUnder (· ≤ ·) l fun x => (u x)⁻¹) ↔ IsBoundedUnder (· ≥ ·) l u :=
  (OrderIso.inv α).isBoundedUnder_ge_comp

Похожие утверждения