upperSemicontinuousOn_iff_isClosed_hypograph

English

If s is closed and f: α → γ, then f is upper semicontinuous on s if and only if the hypograph { (a,t) | a ∈ s and t ≤ f(a) } is closed in α × γ.

Русский

Если s замкнуто и f: α → γ, то f имеет верхнюю полупрерывность на s тогда и только тогда, когда гипограф { (a,t) | a ∈ s и t ≤ f(a) } замкнут в α × γ.

LaTeX

$$$\\text{UpperSemicontinuousOn}(f,s) \\iff \\text{IsClosed}\\{(a,t)\\in α×γ : a\\in s \\land t \\le f(a)\\}.$$$

Lean4

theorem upperSemicontinuousOn_iff_isClosed_hypograph {f : α → γ} (hs : IsClosed s) :
    UpperSemicontinuousOn f s ↔ IsClosed {p : α × γ | p.1 ∈ s ∧ p.2 ≤ f p.1} :=
  lowerSemicontinuousOn_iff_isClosed_epigraph hs (γ := γᵒᵈ)

Похожие утверждения