isClosed_antitoneOn — Mathlib

English

For any s, the set { f : β → α | AntitoneOn f s } is closed, taking αᵒᵈ as the reversed order.

Русский

Для любого множества s множество { f : β → α | AntitoneOn f s } замкнуто, используя двойственный порядок.

LaTeX

$$$ \\text{IsClosed} \\{ f:\\beta \\to \\alpha \\mid \\text{AntitoneOn } f \\; s \\} $$$

Lean4

/-- The set of antitone functions on a set is closed. -/
theorem isClosed_antitoneOn [Preorder β] {s : Set β} : IsClosed {f : β → α | AntitoneOn f s} :=
  isClosed_monotoneOn (α := αᵒᵈ) (β := β)

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