upperSemicontinuous_iff_IsClosed_hypograph

English

A function f: α → γ is upper semicontinuous if and only if the hypograph { (x,y) | y ≤ f(x) } is closed in α × γ, under appropriate order/topology assumptions on γ.

Русский

Функция f: α → γ имеет верхнюю полупрерывность тогда и только тогда, когда гипограф { (x,y) | y ≤ f(x) } замкнут в α × γ при соответствующих предположениях о порядке и топологии γ.

LaTeX

$$$\\text{UpperSemicontinuous}(f) \\iff \\text{IsClosed}\\{(x,y)\\in α×γ \\mid y \\le f(x)\\}. $$$

Lean4

theorem upperSemicontinuous_iff_IsClosed_hypograph {f : α → γ} :
    UpperSemicontinuous f ↔ IsClosed {p : α × γ | p.2 ≤ f p.1} :=
  lowerSemicontinuous_iff_isClosed_epigraph (γ := γᵒᵈ)

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