Theorems · Definition · general topology

Urysohns.CU.left

{X : Type u_1} → [inst : TopologicalSpace X] → {P : Set X → Set X → Prop} → Urysohns.CU P → Urysohns.CU P

By assumption, for each c : CU P there exists an open set u such that c.C ⊆ u and closure u ⊆ c.U. c.left is the pair (c.C, u).

Defined in

Mathlib.Topology.UrysohnsLemma

Cited by

13 results in Mathlib

Foundations

Depth 11 from the axioms · uses Classical.choice

Assumes

TopologicalSpace