English
For any set s in β, the collection { f: β → α | MonotoneOn f s } is a closed subset of the function space with the order topology.
Русский
Для множества s ⊆ β множество функций { f: β→α | MonotoneOn f s } замкнуто в пространстве функций с топологией порядка.
LaTeX
$$$ \\text{IsClosed} \\bigl\\{ f:\\beta \\to \\alpha \\mid \\text{MonotoneOn } f \\; s \\bigr\\} $$$
Lean4
/-- The set of monotone functions on a set is closed. -/
theorem isClosed_monotoneOn [Preorder β] {s : Set β} : IsClosed {f : β → α | MonotoneOn f s} :=
by
simp only [isClosed_iff_clusterPt, clusterPt_principal_iff_frequently]
intro g hg a ha b hb hab
have hmain (x) : Tendsto (fun f' ↦ f' x) (𝓝 g) (𝓝 (g x)) := continuousAt_apply x _
exact le_of_tendsto_of_tendsto_of_frequently (hmain a) (hmain b) (hg.mono fun g h ↦ h ha hb hab)
