Commit 2023-05-30 06:20 80772540

View on Github →

feat: port Topology.TietzeExtension (#4246)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/TietzeExtension.lean

added theorem BoundedContinuousFunction.exists_extension_forall_exists_le_ge_of_closedEmbedding

added theorem BoundedContinuousFunction.exists_extension_forall_mem_Icc_of_closedEmbedding

added theorem BoundedContinuousFunction.exists_extension_forall_mem_of_closedEmbedding

added theorem BoundedContinuousFunction.exists_extension_norm_eq_of_closedEmbedding'

added theorem BoundedContinuousFunction.exists_extension_norm_eq_of_closedEmbedding

added theorem BoundedContinuousFunction.exists_forall_mem_restrict_eq_of_closed

added theorem BoundedContinuousFunction.exists_norm_eq_restrict_eq_of_closed

added theorem BoundedContinuousFunction.tietze_extension_step

added theorem ContinuousMap.exists_extension_forall_mem_of_closedEmbedding

added theorem ContinuousMap.exists_extension_of_closedEmbedding

added theorem ContinuousMap.exists_restrict_eq_forall_mem_of_closed

added theorem ContinuousMap.exists_restrict_eq_of_closed