upperSemicontinuousAt

Mathlib.Topology.Semicontinuous

URI: https://scilib.ai/kg/mathlib#ContinuousAt.upperSemicontinuousAt

English

A USC at a point x is equivalent to limsup of f along nhds at x being ≤ f(x).

Русский

УСЦ в точке x эквивалентно тому, что limsup f вдоль nhds в x меньше или равно f(x).

LaTeX

$$$\\mathrm{UpperSemicontinuousAt}(f,x) \\iff \\limsup f (\\mathcal{N}(x)) \\le f(x)$$$

Lean4

theorem upperSemicontinuousAt {f : α → γ} (h : ContinuousAt f x) : UpperSemicontinuousAt f x := fun _y hy =>
  h (Iio_mem_nhds hy)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru