Theorems · Definition · general topology
Urysohns.CU.C
{X : Type u_2} → [inst : TopologicalSpace X] → {P : Set X → Set X → Prop} → Urysohns.CU P → Set XThe inner set in the inductive construction towards Urysohn's lemma
- Defined in
- Mathlib.Topology.UrysohnsLemma
- Cited by
- 11 results in Mathlib
- Foundations
- Depth 2 from the axioms · uses no axioms
- Assumes
- TopologicalSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- TopologicalSpacestatement and proof · cited by 24,529
- Urysohns.CUstatement and proof · cited by 36
Cited by12
Results whose statement or proof uses this declaration.
- Urysohns.CU.leftproof · cited by 13
- Urysohns.CU.lim_of_mem_Cstatement and proof · cited by 4
- Urysohns.CU.subsetstatement · cited by 4
- Urysohns.CU.continuous_limproof · cited by 3
- Urysohns.CU.left_U_subset_right_Cstatement · cited by 3
- Urysohns.CU.approx_of_mem_Cstatement and proof · cited by 2
- Urysohns.CU.closed_Cstatement · cited by 1
- Urysohns.CU.disjoint_C_support_limstatement and proof · cited by 1
- Urysohns.CU.approx_le_approx_of_U_sub_Cstatement and proof · cited by 1
- Urysohns.CU.subset_right_Cstatement · cited by 1
- Urysohns.CU.left_Cstatement and proof · cited by 0
- Urysohns.CU.P_C_Ustatement · cited by 0