fixedPoints_submonoid_iSup — Mathlib

English

Fixed points of an indexed supremum equals the intersection of fixed points over the index set.

Русский

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

LaTeX

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

Lean4

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

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