sInf_inv — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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