English
If s is closed and f is continuous on s, then the epigraph of f over s, i.e., { (b,t) ∈ β×α : b ∈ s ∧ f(b) ≤ t }, is a closed subset of β×α.
Русский
Если s замкнуто и f непрерывна на s, то эпиграф функции f над s, то есть множество { (b,t) ∈ β×α : b ∈ s и f(b) ≤ t }, замкнуто в β×α.
LaTeX
$$$ \\text{IsClosed}(s) \\Rightarrow \\text{IsClosed}({(b,t) \\in \\beta \\times \\alpha \\mid b \\in s \\land f(b) \\le t}) $$$
Lean4
theorem epigraph [TopologicalSpace β] {f : β → α} {s : Set β} (hs : IsClosed s) (hf : ContinuousOn f s) :
IsClosed {p : β × α | p.1 ∈ s ∧ f p.1 ≤ p.2} :=
(hs.preimage continuous_fst).isClosed_le (hf.comp continuousOn_fst Subset.rfl) continuousOn_snd
