fixingSubmonoid_union — Mathlib

English

The fixing submonoid of a union equals the intersection of fixing submonoids.

Русский

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

LaTeX

$$$fixingSubmonoid(M, s \\cup t) = fixingSubmonoid(M,s) \\cap fixingSubmonoid(M,t)$$$

Lean4

/-- Fixing submonoid of union is intersection -/
@[to_additive]
theorem fixingSubmonoid_union {s t : Set α} : fixingSubmonoid M (s ∪ t) = fixingSubmonoid M s ⊓ fixingSubmonoid M t :=
  (fixingSubmonoid_fixedPoints_gc M α).l_sup

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