Theorems · Definition · general topology

UpperSemicontinuous

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

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 + ε.

Defined in

Mathlib.Topology.Semicontinuity.Defs

Cited by

52 results in Mathlib

Foundations

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

Assumes

TopologicalSpacePreorder