fixingSubmonoid_antitone — Mathlib

English

FixingSubmonoid is antitone in the fixed set: enlarging s decreases the fixing submonoid.

Русский

Фиксирующий подмоноид зависим от множества: увеличение множества снижает фиксацию подмоноида.

LaTeX

$$$s \\subseteq t \\quad\\Rightarrow\\quad fixingSubmonoid(M,t) \\le fixingSubmonoid(M,s)$$$

Lean4

@[to_additive]
theorem fixingSubmonoid_antitone : Antitone fun s : Set α => fixingSubmonoid M s :=
  (fixingSubmonoid_fixedPoints_gc M α).monotone_l

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