Structure Urysohns.CU

Modification history

2025-04-21 11:07
Mathlib/Topology/UrysohnsLemma.lean
feat: modify Urysohn's lemma to let `P` depend on `U` (#24179) …
Modified Urysohns.CUView on Github →
2023-11-07 10:06
Mathlib/Topology/UrysohnsLemma.lean
feat: Urysohn lemma in regular locally compact spaces (#8124) …
Modified Urysohns.CUView on Github →
2023-08-10 19:52
Mathlib/Topology/UrysohnsLemma.lean
chore: banish `Type _` and `Sort _` (#6499) …
Modified Urysohns.CUView on Github →
2023-04-18 03:37
Mathlib/Topology/UrysohnsLemma.lean
feat: port Topology.UrysohnsLemma (#3490)
Added Urysohns.CUView on Github →