Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-22 12:04 af683b11

View on Github →

feat(topology/tietze_extension): Tietze extension theorem (#10701)

Estimated changes

Created src/data/set/intervals/monotone.lean

added theorem monotone_of_odd_of_monotone_on_nonneg

added def order_iso_Ioo_neg_one_one

added theorem strict_mono_of_odd_strict_mono_on_nonneg

Modified src/order/hom/basic.lean

added def strict_mono.order_iso_of_right_inverse

Modified src/topology/continuous_function/bounded.lean

added theorem bounded_continuous_function.norm_comp_continuous_le

Created src/topology/tietze_extension.lean

added theorem bounded_continuous_function.exists_extension_forall_exists_le_ge_of_closed_embedding

added theorem bounded_continuous_function.exists_extension_forall_mem_Icc_of_closed_embedding

added theorem bounded_continuous_function.exists_extension_forall_mem_of_closed_embedding

added theorem bounded_continuous_function.exists_extension_norm_eq_of_closed_embedding'

added theorem bounded_continuous_function.exists_extension_norm_eq_of_closed_embedding

added theorem bounded_continuous_function.exists_forall_mem_restrict_eq_of_closed

added theorem bounded_continuous_function.exists_norm_eq_restrict_eq_of_closed

added theorem bounded_continuous_function.tietze_extension_step

added theorem continuous_map.exists_extension_forall_mem_of_closed_embedding

added theorem continuous_map.exists_extension_of_closed_embedding

added theorem continuous_map.exists_restrict_eq_forall_mem_of_closed

added theorem continuous_map.exists_restrict_eq_of_closed

Modified src/topology/urysohns_bounded.lean