unop_sInf — Mathlib

English

Let S be a set of submonoids of the opposite monoid M^{op}. Then (sInf S).unop = sInf (op^{-1} S).

Русский

Пусть S — множество подмонодов противоположного моноида M^{op}. Тогда (sInf S).unop = sInf (op^{-1} S).

LaTeX

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

Lean4

@[to_additive]
theorem unop_sInf (S : Set (Submonoid Mᵐᵒᵖ)) : (sInf S).unop = sInf (.op ⁻¹' S) :=
  opEquiv.symm.map_sInf_eq_sInf_symm_preimage _

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