Theorems · Theorem · general topology

exists_mem_nhds_isCompact_mapsTo_of_isCompact_mem_nhds

∀ {X : Type u_3} {Y : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [R1Space Y] {f : X → Y}
  {x : X} {K : Set X} {s : Set Y},
  Continuous f → s ∈ nhds (f x) → IsCompact K → K ∈ nhds x → ∃ L ∈ nhds x, IsCompact L ∧ Set.MapsTo f L s

Defined in

Mathlib.Topology.Separation.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpaceR1Space