UpperSemicontinuousWithinAt — Mathlib

English

A function is upper semicontinuous at x if for every y > f(x), f(x') < y holds eventually near x.

Русский

Функция верхнеполуанепрерывна в точке x, если для любого y > f(x) существует окрестность, в которой f(x') < y.

LaTeX

$$UpperSemicontinuousAt f x := ∀ y, f x < y → ∀ᶠ x' in nhds x, f x' < y$$

Lean4

/-- A real function `f` is upper semicontinuous at `x` within a set `s` if, for any `ε > 0`, for all
`x'` close enough to `x` in `s`, then `f x'` is at most `f x + ε`. We formulate this in a general
preordered space, using an arbitrary `y > f x` instead of `f x + ε`. -/
def UpperSemicontinuousWithinAt (f : α → β) (s : Set α) (x : α) :=
  ∀ y, f x < y → ∀ᶠ x' in 𝓝[s] x, f x' < y

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