Theorems · Theorem · general topology

lowerSemicontinuousWithinAt_iff_le_liminf

∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {x : α} {γ : Type u_4} [inst_1 : CompleteLinearOrder γ]
  {f : α → γ}, LowerSemicontinuousWithinAt f s x ↔ f x ≤ Filter.liminf f (nhdsWithin x s)

Defined in

Mathlib.Topology.Semicontinuity.Basic

Cited by

3 results in Mathlib

Foundations

Depth 51 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceCompleteLinearOrder