Theorems · Definition · general topology

LowerSemicontinuous

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

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

Defined in

Mathlib.Topology.Semicontinuity.Defs

Cited by

69 results in Mathlib

Foundations

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

Assumes

TopologicalSpacePreorder