UpperSemicontinuous — Mathlib

English

Definitions for upper semicontinuity on sets and at points.

Русский

Определения верхней полупрерывности на множествах и в точках.

LaTeX

$$UpperSemicontinuous f = ∀ x, UpperSemicontinuousAt f x$$

Lean4

/-- A real function `f` is upper semicontinuous if, for any `ε > 0`, for any `x`, for all `x'`
close enough to `x`, 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 UpperSemicontinuous (f : α → β) :=
  ∀ x, UpperSemicontinuousAt f x

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