Theorems · Theorem · general topology

exists_continuousMap_one_of_isCompact_subset_isOpen

∀ {X : Type u_1} [inst : TopologicalSpace X] [R1Space X] [LocallyCompactSpace X] {K V : Set X},
  IsCompact K →
    IsOpen V → K ⊆ V → ∃ f, Set.EqOn (⇑f) 1 K ∧ IsCompact (tsupport ⇑f) ∧ tsupport ⇑f ⊆ V ∧ ∀ (x : X), f x ∈ Set.Icc 0 1

A variation of Urysohn's lemma. In a Hausdorff locally compact space, for a compact set K contained in an open set V, there exists a compactly supported continuous function f such that 0 ≤ f ≤ 1, f = 1 on K and the support of f is contained in V.

Defined in

Mathlib.Topology.UrysohnsLemma

Cited by

3 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceR1SpaceLocallyCompactSpace