isClosed_antitone — Mathlib

English

The set { f : β → α | Antitone f } is closed, i.e., the family of anti-monotone functions is closed in the appropriate function space.

Русский

Множество функций { f : β → α | Antitone f } замкнуто в пространстве функций.

LaTeX

$$$ \\text{IsClosed} \\{ f:\\beta \\to \\alpha \\mid \\text{Antitone } f \\} $$$

Lean4

/-- The set of antitone functions is closed. -/
theorem isClosed_antitone [Preorder β] : IsClosed {f : β → α | Antitone f} :=
  isClosed_monotone (α := αᵒᵈ) (β := β)

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