Commit 2023-06-24 05:23 60d0908c

View on Github →

feat: port Geometry.Manifold.BumpFunction (#5437)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Geometry/Manifold/BumpFunction.lean

added theorem SmoothBumpFunction.ball_inter_range_eq_ball_inter_target

added theorem SmoothBumpFunction.ball_subset

added theorem SmoothBumpFunction.c_mem_support

added theorem SmoothBumpFunction.coe_def

added theorem SmoothBumpFunction.eqOn_source

added theorem SmoothBumpFunction.eq_one

added theorem SmoothBumpFunction.eventuallyEq_of_mem_source

added theorem SmoothBumpFunction.eventuallyEq_one

added theorem SmoothBumpFunction.eventuallyEq_one_of_dist_lt

added theorem SmoothBumpFunction.exists_r_pos_lt_subset_ball

added theorem SmoothBumpFunction.image_eq_inter_preimage_of_subset_support

added theorem SmoothBumpFunction.isClosed_image_of_isClosed

added theorem SmoothBumpFunction.isClosed_symm_image_closedBall

added theorem SmoothBumpFunction.isCompact_symm_image_closedBall

added theorem SmoothBumpFunction.isOpen_support

added theorem SmoothBumpFunction.le_one

added theorem SmoothBumpFunction.mem_Icc

added theorem SmoothBumpFunction.nhdsWithin_range_basis

added theorem SmoothBumpFunction.nhds_basis_support

added theorem SmoothBumpFunction.nhds_basis_tsupport

added theorem SmoothBumpFunction.nonempty_support

added theorem SmoothBumpFunction.nonneg

added theorem SmoothBumpFunction.one_of_dist_le

added theorem SmoothBumpFunction.rOut_pos

added theorem SmoothBumpFunction.smooth_smul

added theorem SmoothBumpFunction.support_eq_inter_preimage

added theorem SmoothBumpFunction.support_eq_symm_image

added theorem SmoothBumpFunction.support_mem_nhds

added theorem SmoothBumpFunction.support_subset_source

added theorem SmoothBumpFunction.support_updateRIn

added def SmoothBumpFunction.toFun

added theorem SmoothBumpFunction.tsupport_mem_nhds

added theorem SmoothBumpFunction.tsupport_subset_chartAt_source

added theorem SmoothBumpFunction.tsupport_subset_extChartAt_source

added theorem SmoothBumpFunction.tsupport_subset_symm_image_closedBall

added def SmoothBumpFunction.updateRIn

added structure SmoothBumpFunction