Theorems · Theorem · general topology

ContinuousAt.comp_upperSemicontinuousAt

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

Defined in

Mathlib.Topology.Semicontinuity.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceLinearOrderTopologicalSpaceOrderTopologyLinearOrderTopologicalSpaceOrderTopology