range_inv — Mathlib

English

If a range is bounded above, then the range of inverses is bounded below.

Русский

Если диапазон ограничен сверху, то диапазон инверсий ограничен снизу.

LaTeX

$$BddAbove (range f) \Rightarrow BddBelow (range (\lambda x, f x)^{-1})$$

Lean4

@[to_additive]
theorem range_inv {α : Type*} {f : α → G} (hf : BddAbove (range f)) : BddBelow (range (fun x => (f x)⁻¹)) :=
  BddBelow.range_inv (G := Gᵒᵈ) hf

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