fixedPoints_antitone — Mathlib

English

The assignment P ↦ fixedPoints(P,α) is antitone: larger P yields smaller fixed point set.

Русский

Отображение P ↦ fixedPoints(P, α) антимонотно: больший P даёт меньший набор фиксированных точек.

LaTeX

$$$P \\subseteq Q \\Rightarrow fixedPoints(P,\\alpha) \\supseteq fixedPoints(Q,\\alpha)$$$

Lean4

@[to_additive fixedPoints_antitone_addSubmonoid]
theorem fixedPoints_antitone : Antitone fun P : Submonoid M => fixedPoints P α :=
  (fixingSubmonoid_fixedPoints_gc M α).monotone_u.dual_left

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