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