English
Let f, g : β → α with h: f ≤ g on s and hf, hg continuous on closure s. Then for any x ∈ closure s, f(x) ≤ g(x).
Русский
Пусть f, g : β → α, s ⊆ β, h: ∀ y ∈ s, f(y) ≤ g(y); hf, hg непрерывны на closure(s). Тогда для любого x ∈ closure(s) выполняется f(x) ≤ g(x).
LaTeX
$$$ (\\forall y\\in s:\\ f(y) \\le g(y)) \\land \\text{ContinuousOn}(f,\\overline{s}) \\land \\text{ContinuousOn}(g,\\overline{s}) \\Rightarrow f(x) \\le g(x) \\text{ для всех } x \\in \\overline{s} $$$
Lean4
theorem le_on_closure [TopologicalSpace β] {f g : β → α} {s : Set β} (h : ∀ x ∈ s, f x ≤ g x)
(hf : ContinuousOn f (closure s)) (hg : ContinuousOn g (closure s)) ⦃x⦄ (hx : x ∈ closure s) : f x ≤ g x :=
have : s ⊆ {y ∈ closure s | f y ≤ g y} := fun y hy => ⟨subset_closure hy, h y hy⟩
(closure_minimal this (isClosed_closure.isClosed_le hf hg) hx).2
