Theorems · Definition · general topology

Semicontinuous

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

A relation r : α → β → Prop is semicontinuous if it is semicontinuous within s at each x : α.

Defined in

Mathlib.Topology.Semicontinuity.Defs

Cited by

12 results in Mathlib

Foundations

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

Assumes

TopologicalSpace