op_sInf — Mathlib

English

The opposite of the infimum of a set of subgroups equals the infimum of the preimage under unop.

Русский

Противоположная операция сохраняет наименьшую грань через предобразие unop: (sInf S)^{op} = sInf (unop ⁻¹' S).

LaTeX

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

Lean4

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

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