English
A function is lower semicontinuous at x within s if for every y < f(x), f(x') > y eventually for x' in neighborhoods within s.
Русский
Функция ниже полунепрерывна в точке x внутри множества s, если для любого y < f(x) верно, что для соседей x внутри s f(x') > y встречается часто.
LaTeX
$$LowerSemicontinuousWithinAt f s x := ∀ y < f x, ∀ᶠ x' in nhdsWithin x s, y < f x'$$
Lean4
/-- A real function `f` is lower semicontinuous if, for any `ε > 0`, for any `x`, for all `x'` close
enough to `x`, then `f x'` is at least `f x - ε`. We formulate this in a general preordered space,
using an arbitrary `y < f x` instead of `f x - ε`. -/
def LowerSemicontinuous (f : α → β) :=
∀ x, LowerSemicontinuousAt f x
