UpperSemicontinuousOn — Mathlib

English

A function is upper semicontinuous on a set s if it is upper semicontinuous at every point of s.

Русский

Функция верхнеполу анепрерывна на множестве s, если она такова в каждой точке из s.

LaTeX

$$UpperSemicontinuousOn f s := ∀ x ∈ s, UpperSemicontinuousWithinAt f s x$$

Lean4

/-- A real function `f` is upper semicontinuous on a set `s` if, for any `ε > 0`, for any `x ∈ s`,
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 UpperSemicontinuousOn (f : α → β) (s : Set α) :=
  ∀ x ∈ s, UpperSemicontinuousWithinAt f s x

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