Theorems · Theorem · general topology

UpperHemicontinuousAt.isInducing_comp

∀ {α : Type u_3} {β : Type u_4} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → Set β} {x : α}
  {γ : Type u_5} [inst_2 : TopologicalSpace γ] {i : γ → β},
  UpperHemicontinuousAt f x →
    Topology.IsInducing i → IsClosed (Set.range i) → UpperHemicontinuousAt (fun x => i ⁻¹' f x) x

Post-composition with the preimage of an inducing function whose range is closed preserves upper hemicontinuity.

Defined in

Mathlib.Topology.Semicontinuity.Hemicontinuity

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpaceTopologicalSpace