Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-04 14:00 338331e2

View on Github →

feat(topology/urysohns_lemma): Urysohn's lemma (#6967)

Estimated changes

Modified src/algebra/ordered_ring.lean

added theorem inv_of_le_one

added theorem inv_of_lt_zero

added theorem inv_of_nonneg

added theorem inv_of_nonpos

added theorem inv_of_pos

Modified src/analysis/normed_space/add_torsor.lean

added theorem dist_midpoint_midpoint_le'

added theorem dist_midpoint_midpoint_le

added theorem filter.tendsto.line_map

added theorem filter.tendsto.midpoint

Modified src/data/indicator_function.lean

added theorem set.indicator_diff

modified theorem set.le_mul_indicator_apply

modified theorem set.mul_indicator_apply_le'

modified theorem set.mul_indicator_compl

added theorem set.mul_indicator_diff

Modified src/linear_algebra/affine_space/midpoint.lean

added theorem midpoint_eq_smul_add

Modified src/linear_algebra/affine_space/ordered.lean

added theorem midpoint_le_midpoint

Modified src/topology/metric_space/basic.lean

added theorem metric.nhds_basis_ball_pow

added theorem metric.nhds_basis_closed_ball_pow

added theorem metric.uniformity_basis_dist_le_pow

added theorem metric.uniformity_basis_dist_pow

added theorem real.dist_le_of_mem_Icc

added theorem real.dist_le_of_mem_Icc_01

added theorem real.dist_le_of_mem_interval

added theorem real.dist_left_le_of_mem_interval

added theorem real.dist_right_le_of_mem_interval

Created src/topology/urysohns_lemma.lean

added theorem exists_continuous_zero_one_of_closed

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.bdd_above_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_at_top

added structure urysohns.CU