fixedPoints_subgroup_iSup — Mathlib

English

There is a Galois connection between fixingSubgroup M and fixedPoints P α

Русский

Существует связь Галуа между fixingSubgroup M и fixedPoints P α.

LaTeX

$$$\\text{GaloisConnection}(OrderDual.toDual \\circ fixingSubgroup M, (\\lambda P: Subgroup M. fixedPoints P α) \\circ OrderDual.ofDual)$$$

Lean4

/-- Fixed points of iSup of subgroups is intersection -/
@[to_additive]
theorem fixedPoints_subgroup_iSup {ι : Sort*} {P : ι → Subgroup M} :
    fixedPoints (↥(iSup P)) α = ⋂ i, fixedPoints (P i) α :=
  (fixingSubgroup_fixedPoints_gc M α).u_iInf

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