isClosed_monotone — Mathlib

English

The set { f : β → α | Monotone f } is closed in the space of all functions β → α with the order-closed topology on α.

Русский

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

LaTeX

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

Lean4

/-- The set of monotone functions is closed. -/
theorem isClosed_monotone [Preorder β] : IsClosed {f : β → α | Monotone f} :=
  by
  simp_rw [← monotoneOn_univ]
  exact isClosed_monotoneOn

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