Commit 2025-12-18 07:31 524aa25d

View on Github →

chore: deprecate smooth variants of contMDiff results (#31326)

Estimated changes

Modified Mathlib/Analysis/Calculus/BumpFunction/FiniteDimension.lean

added theorem IsOpen.exists_contDiff_support_eq

deleted theorem IsOpen.exists_smooth_support_eq

added theorem exists_contDiff_tsupport_subset

deleted theorem exists_smooth_tsupport_subset

Modified Mathlib/Analysis/Distribution/AEEqOfIntegralContDiff.lean

added theorem IsOpen.ae_eq_zero_of_integral_contMDiff_smul_eq_zero'

added theorem IsOpen.ae_eq_zero_of_integral_contMDiff_smul_eq_zero

deleted theorem IsOpen.ae_eq_zero_of_integral_smooth_smul_eq_zero

added theorem ae_eq_of_integral_contMDiff_smul_eq

deleted theorem ae_eq_of_integral_smooth_smul_eq

added theorem ae_eq_zero_of_integral_contMDiff_smul_eq_zero

deleted theorem ae_eq_zero_of_integral_smooth_smul_eq_zero

Modified Mathlib/Geometry/Manifold/IsManifold/Basic.lean

Modified Mathlib/Geometry/Manifold/PartitionOfUnity.lean

added theorem Emetric.exists_contMDiffMap_forall_closedBall_subset

deleted theorem Emetric.exists_smooth_forall_closedBall_subset

added theorem IsOpen.exists_contMDiff_support_eq

added theorem IsOpen.exists_contMDiff_support_eq_aux

deleted theorem IsOpen.exists_msmooth_support_eq

deleted theorem IsOpen.exists_msmooth_support_eq_aux

added theorem Metric.exists_contMDiffMap_forall_closedBall_subset

deleted theorem Metric.exists_smooth_forall_closedBall_subset

added theorem exists_contMDiffMap_forall_mem_convex_of_local

added theorem exists_contMDiffMap_forall_mem_convex_of_local_const

added theorem exists_contMDiffMap_one_nhds_of_subset_interior

added theorem exists_contMDiffMap_zero_one_nhds_of_isClosed

added theorem exists_contMDiffMap_zero_one_of_isClosed

deleted theorem exists_contMDiffOn_forall_mem_convex_of_local

deleted theorem exists_contMDiffOn_section_forall_mem_convex_of_local

added theorem exists_contMDiffSection_forall_mem_convex_of_local

added theorem exists_contMDiff_support_eq_eq_one_iff

added theorem exists_contMDiff_zero_iff_one_iff_of_isClosed

deleted theorem exists_msmooth_support_eq_eq_one_iff

deleted theorem exists_msmooth_zero_iff_one_iff_of_isClosed

deleted theorem exists_smooth_forall_mem_convex_of_local

deleted theorem exists_smooth_forall_mem_convex_of_local_const

deleted theorem exists_smooth_one_nhds_of_subset_interior

deleted theorem exists_smooth_section_forall_mem_convex_of_local

deleted theorem exists_smooth_zero_one_nhds_of_isClosed

deleted theorem exists_smooth_zero_one_of_isClosed

Modified Mathlib/Geometry/Manifold/SmoothApprox.lean