upperSemicontinuousWithinAt — Mathlib

English

A WithinAt USC condition is equivalent to having limsup ≤ f(x) with respect to nhds inside s.

Русский

Условие USC внутри точки эквивалентно не превышению limsup по nhds внутри области s.

LaTeX

$$$\\mathrm{UpperSemicontinuousWithinAt}(f,s,x) \\iff \\limsup f (\\mathcal{N}_s(x)) \\le f(x)$$$

Lean4

theorem upperSemicontinuousWithinAt {f : α → γ} (h : ContinuousWithinAt f s x) : UpperSemicontinuousWithinAt f s x :=
  fun _y hy => h (Iio_mem_nhds hy)

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