Theorems · Theorem · general topology

lowerSemicontinuousOn_iff_isClosed_epigraph

∀ {α : Type u_1} [inst : TopologicalSpace α] {γ : Type u_4} [inst_1 : LinearOrder γ] [inst_2 : TopologicalSpace γ]
  [ClosedIciTopology γ] {f : α → γ} {s : Set α},
  IsClosed s → (LowerSemicontinuousOn f s ↔ IsClosed {p | p.1 ∈ s ∧ f p.1 ≤ p.2})

Defined in

Mathlib.Topology.Semicontinuity.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceLinearOrderTopologicalSpaceClosedIciTopology