op_sInf — Mathlib

English

Let S be a set of submonoids of a monoid M. The opposite of the infimum of S equals the infimum of the opposites obtained by unop; i.e. (sInf S).op = sInf (unop^{-1} S).

Русский

Пусть S — множество подмонодов Моноида M. Противоположность инфимума множества S равна инфимуму противоположностей, полученных применением unop; тождество (sInf S).op = sInf (unop^{-1} S).

LaTeX

$$$ (\operatorname{sInf}(S))^{\mathrm{op}} = \operatorname{sInf}(\operatorname{unop}^{-1} S) $$$

Lean4

@[to_additive]
theorem op_sInf (S : Set (Submonoid M)) : (sInf S).op = sInf (.unop ⁻¹' S) :=
  opEquiv.map_sInf_eq_sInf_symm_preimage _

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