bddBelow_inv — Mathlib

English

Similarly, inversion swaps upper and lower bounds: if s is bounded below, then s⁻¹ is bounded above.

Русский

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

LaTeX

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

Lean4

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

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