Theorems · Definition · general topology

Urysohns.CU.right

{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.right is the pair (closure u, c.U).

Defined in

Mathlib.Topology.UrysohnsLemma

Cited by

13 results in Mathlib

Foundations

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

Assumes

TopologicalSpace