Theorems · Definition · general topology

LowerHemicontinuousWithinAt

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

A function f : α → Set β is lower hemicontinuous at x within a set s if, whenever t is an open set intersecting f x, then t also intersects f x' for all x' sufficiently close to x within s.

Defined in

Mathlib.Topology.Semicontinuity.Defs

Cited by

15 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpace