bddAbove_inv — Mathlib

English

In a group, the upper bound property is preserved under inversion: if s is bounded above, then s⁻¹ is bounded below.

Русский

В группе верхняя граница сохраняется при взятии обратного: если s ограничено сверху, то s⁻¹ ограничено снизу.

LaTeX

$$BddAbove s \Rightarrow BddBelow s^{-1}$$

Lean4

@[to_additive (attr := simp)]
theorem bddAbove_inv : BddAbove s⁻¹ ↔ BddBelow s :=
  (OrderIso.inv G).bddAbove_preimage

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