Theorems · Theorem · general topology

Continuous.comp_lowerSemicontinuousOn

∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {γ : Type u_4} [inst_1 : LinearOrder γ]
  [inst_2 : TopologicalSpace γ] [OrderTopology γ] {δ : Type u_5} [inst_4 : LinearOrder δ] [inst_5 : TopologicalSpace δ]
  [OrderTopology δ] {g : γ → δ} {f : α → γ},
  Continuous g → LowerSemicontinuousOn f s → Monotone g → LowerSemicontinuousOn (g ∘ f) s

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

TopologicalSpaceLinearOrderTopologicalSpaceOrderTopologyLinearOrderTopologicalSpaceOrderTopology