English
Let α be a topological space equipped with a preorder and OrderClosedTopology. For β a topological space, and f, g : β → α, let s ⊆ β and x ∈ β with x ∈ closure s. If f|s and g|s are continuous at x and f(y) ≤ g(y) for all y ∈ s, then f(x) ≤ g(x).
Русский
Пусть α — топологическое множество с линейным порядком и OrderClosedTopology. Пусть β — топологическое множество, f, g : β → α, s ⊆ β и x ∈ β так, что x ∈ замыкание s. Если ограниченные функции f|s и g|s непрерывны в точке x и выполняется f(y) ≤ g(y) для всякого y ∈ s, то f(x) ≤ g(x).
LaTeX
$$$ \\forall \\beta \\, \\alpha \\, (\\text{TopologicalSpace } \\alpha) \\, (\\text{Preorder } \\alpha) \\, (\\text{OrderClosedTopology } \\alpha) \\, \\forall f,g : \\beta \\to \\alpha \\, \\forall s : \\mathcal{P}(\\beta) \\, \\forall x : \\beta,\\ x \\in \\overline{s} \\, \\wedge\\ (f|_{s}) \\, \\text{is continuous at } x \\, \\wedge\\ (g|_{s}) \\, \\text{is continuous at } x \\, \\wedge\\ (\\forall y \\in s,\\ f(y) \\le g(y)) \\\\Rightarrow\\ f(x) \\le g(x) $$$
Lean4
theorem closure_le [TopologicalSpace β] {f g : β → α} {s : Set β} {x : β} (hx : x ∈ closure s)
(hf : ContinuousWithinAt f s x) (hg : ContinuousWithinAt g s x) (h : ∀ y ∈ s, f y ≤ g y) : f x ≤ g x :=
show (f x, g x) ∈ {p : α × α | p.1 ≤ p.2} from
OrderClosedTopology.isClosed_le'.closure_subset ((hf.prodMk hg).mem_closure hx h)
