Theorems · Theorem · general topology

ContinuousAt.comp_lowerSemicontinuousWithinAt

∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {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) → LowerSemicontinuousWithinAt f s x → Monotone g → LowerSemicontinuousWithinAt (g ∘ f) s x

Defined in

Mathlib.Topology.Semicontinuity.Basic

Cited by

4 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceLinearOrderTopologicalSpaceOrderTopologyLinearOrderTopologicalSpaceOrderTopology