fixingSubgroup_union — Mathlib

English

Fixed points of the join of two submonoids equal the intersection of their fixed points.

Русский

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

LaTeX

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

Lean4

/-- Fixing subgroup of union is intersection -/
@[to_additive]
theorem fixingSubgroup_union {s t : Set α} : fixingSubgroup M (s ∪ t) = fixingSubgroup M s ⊓ fixingSubgroup M t :=
  (fixingSubgroup_fixedPoints_gc M α).l_sup

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