fixingSubmonoid_iUnion — Mathlib

English

The fixing submonoid of an indexed union equals the infimum of the fixing submonoids.

Русский

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

LaTeX

$$$fixingSubmonoid(M, \\bigcup_i s_i) = \\bigwedge_i fixingSubmonoid(M, s_i)$$$

Lean4

/-- Fixing submonoid of iUnion is intersection -/
@[to_additive]
theorem fixingSubmonoid_iUnion {ι : Sort*} {s : ι → Set α} :
    fixingSubmonoid M (⋃ i, s i) = ⨅ i, fixingSubmonoid M (s i) :=
  (fixingSubmonoid_fixedPoints_gc M α).l_iSup

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