Theorems · Definition · general topology

HasOpenLowerSections

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

A function f : α → Set β has open lower sections if, for every b, the set {x | b ∈ f x} is open. Equivalently, whenever b ∈ f x, then b ∈ f x' for all x' sufficiently close to x.

Defined in

Mathlib.Topology.Semicontinuity.Defs

Cited by

12 results in Mathlib

Foundations

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

Assumes

TopologicalSpace