sSup_inv — Mathlib

English

For any set s in a suitable lattice with inversion, the supremum of the inverse set s^{-1} equals the inverse of the infimum of s: sSup(s^{-1}) = (sInf s)^{-1}.

Русский

Для множества s в подходящей решётке с обращением верно: sSup(s^{-1}) = (sInf s)^{-1}.

LaTeX

$$$$ \\operatorname{sSup}(s^{-1}) = (\\operatorname{sInf}(s))^{-1}. $$$$

Lean4

@[to_additive]
theorem sSup_inv (s : Set M) : sSup s⁻¹ = (sInf s)⁻¹ :=
  by
  rw [← image_inv_eq_inv, sSup_image]
  exact ((OrderIso.inv M).map_sInf _).symm

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