csSup_inv — Mathlib

English

If s is nonempty and bounded below, the supremum of s⁻¹ equals the inverse of the infimum of s.

Русский

Если s непусто и ограничено снизу, то sup s⁻¹ равен обратному инфимуму s.

LaTeX

$$s Nonempty → BddBelow s → sSup s^{-1} = (sInf s)^{-1}$$

Lean4

@[to_additive]
theorem csSup_inv (hs₀ : s.Nonempty) (hs₁ : BddBelow s) : sSup s⁻¹ = (sInf s)⁻¹ :=
  by
  rw [← image_inv_eq_inv]
  exact ((OrderIso.inv _).map_csInf' hs₀ hs₁).symm

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