Commit 2023-04-18 03:37 b706a5fd

View on Github →

feat: port Topology.UrysohnsLemma (#3490)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/UrysohnsLemma.lean

added theorem Urysohns.CU.approx_le_approx_of_U_sub_C

added theorem Urysohns.CU.approx_le_lim

added theorem Urysohns.CU.approx_le_one

added theorem Urysohns.CU.approx_le_succ

added theorem Urysohns.CU.approx_mem_Icc_right_left

added theorem Urysohns.CU.approx_mono

added theorem Urysohns.CU.approx_nonneg

added theorem Urysohns.CU.approx_of_mem_C

added theorem Urysohns.CU.approx_of_nmem_U

added theorem Urysohns.CU.bddAbove_range_approx

added theorem Urysohns.CU.continuous_lim

added def Urysohns.CU.left

added theorem Urysohns.CU.left_U_subset

added theorem Urysohns.CU.left_U_subset_right_C

added theorem Urysohns.CU.lim_eq_midpoint

added theorem Urysohns.CU.lim_le_one

added theorem Urysohns.CU.lim_mem_Icc

added theorem Urysohns.CU.lim_nonneg

added theorem Urysohns.CU.lim_of_mem_C

added theorem Urysohns.CU.lim_of_nmem_U

added def Urysohns.CU.right

added theorem Urysohns.CU.subset_right_C

added theorem Urysohns.CU.tendsto_approx_atTop

added structure Urysohns.CU

added theorem exists_continuous_zero_one_of_closed