English
If s is a closed subset of β and f, g are continuous on s, then the set {x ∈ s | f(x) ≤ g(x)} is closed (in the subspace topology on s).
Русский
Если S — замкнутое подмножество β, а функции f и g непрерывны на S, то множество {x ∈ S | f(x) ≤ g(x)} замкнуто в подпространстве S.
LaTeX
$$$ \\text{IsClosed}(s) \\land \\text{ContinuousOn}(f,s) \\land \\text{ContinuousOn}(g,s) \\Rightarrow \\text{IsClosed}({x \\in s \\mid f(x) \\le g(x)}) $$$
Lean4
/-- If `s` is a closed set and two functions `f` and `g` are continuous on `s`,
then the set `{x ∈ s | f x ≤ g x}` is a closed set. -/
theorem isClosed_le [TopologicalSpace β] {f g : β → α} {s : Set β} (hs : IsClosed s) (hf : ContinuousOn f s)
(hg : ContinuousOn g s) : IsClosed ({x ∈ s | f x ≤ g x}) :=
(hf.prodMk hg).preimage_isClosed_of_isClosed hs OrderClosedTopology.isClosed_le'
