Theorems · Theorem · general topology

Continuous.comp_upperSemicontinuous

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

Defined in

Mathlib.Topology.Semicontinuity.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceLinearOrderTopologicalSpaceOrderTopologyLinearOrderTopologicalSpaceOrderTopology