fixedPoints_subgroup_sup — Mathlib

English

Fixed points of the iSup of subgroups equal the intersection of fixed points over the index.

Русский

Фиксированные точки iSup подгрупп равны пересечению фиксированных точек по индексу.

LaTeX

$$$fixedPoints(\\,iSup_i P(i)\\, , \\alpha) = \\bigcap_i fixedPoints(P(i),\\alpha)$$$

Lean4

/-- Fixed points of sup of subgroups is intersection -/
@[to_additive]
theorem fixedPoints_subgroup_sup {P Q : Subgroup M} : fixedPoints (↥(P ⊔ Q)) α = fixedPoints P α ∩ fixedPoints Q α :=
  (fixingSubgroup_fixedPoints_gc M α).u_inf

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