fixedPoints_submonoid_sup — Mathlib

English

Fixed points of the supremum (join) of submonoids is the intersection of fixed points.

Русский

Фиксированные точки над верхней гранью объединения подмоноидов равны пересечению фиксированных точек.

LaTeX

$$$fixedPoints(\\,P \\sqcup Q\\, , \\alpha) = fixedPoints(P,\\alpha) \\cap fixedPoints(Q,\\alpha)$$$

Lean4

/-- Fixed points of sup of submonoids is intersection -/
@[to_additive]
theorem fixedPoints_submonoid_sup {P Q : Submonoid M} : fixedPoints (↥(P ⊔ Q)) α = fixedPoints P α ∩ fixedPoints Q α :=
  (fixingSubmonoid_fixedPoints_gc M α).u_inf

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