Commit 2023-05-22 16:36 a68b0a8d

View on Github →

feat: port Topology.UrysohnsBounded (#4190)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/UrysohnsBounded.lean

added theorem exists_bounded_mem_Icc_of_closed_of_le

added theorem exists_bounded_zero_one_of_closed