Theorems · Definition · general topology

UpperSemicontinuousAt

{α : Type u_1} → {β : Type u_2} → [TopologicalSpace α] → [Preorder β] → (α → β) → α → Prop

A real function f is upper semicontinuous at x if, for any ε > 0, 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 + ε.

Defined in

Mathlib.Topology.Semicontinuity.Defs

Cited by

35 results in Mathlib

Foundations

Depth 20 from the axioms · uses propext, Quot.sound

Assumes

TopologicalSpacePreorder