Theorems · Inductive type · general topology

Urysohns.CU

{X : Type u_2} → [TopologicalSpace X] → (Set X → Set X → Prop) → Type u_2

An auxiliary type for the proof of Urysohn's lemma: a pair of a closed set C and its open neighborhood U, together with the assumption that C and U satisfy the property P C U. The latter assumption will make it possible to prove simultaneously both versions of Urysohn's lemma, in normal spaces (with P always true) and in locally compact spaces (with P C U = IsCompact C). We put also in the structure the assumption that, for any such pair, one may find an intermediate pair in between satisfying P, to avoid carrying it around in the argument.

Defined in

Mathlib.Topology.UrysohnsLemma

Cited by

36 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms

Assumes

TopologicalSpace