Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-22 13:18 8413f078

View on Github →

feat(topology/support): define topological support and compactly supported functions (#11923)

Also add some variants of the extreme value theorem.

Estimated changes

Modified src/algebra/group/to_additive.lean

Modified src/analysis/calculus/specific_functions.lean

deleted theorem times_cont_diff_bump.closure_support_eq

deleted theorem times_cont_diff_bump.compact_closure_support

deleted theorem times_cont_diff_bump.exists_closure_support_subset

added theorem times_cont_diff_bump.exists_tsupport_subset

added theorem times_cont_diff_bump.tsupport_eq

Modified src/analysis/normed/group/basic.lean

added theorem continuous.bounded_above_of_compact_support

added theorem has_compact_support_norm_iff

Modified src/geometry/manifold/bump_function.lean

deleted theorem smooth_bump_function.closure_support_mem_nhds

deleted theorem smooth_bump_function.closure_support_subset_chart_at_source

deleted theorem smooth_bump_function.closure_support_subset_ext_chart_at_source

deleted theorem smooth_bump_function.closure_support_subset_symm_image_closed_ball

deleted theorem smooth_bump_function.compact_closure_support

deleted theorem smooth_bump_function.nhds_basis_closure_support

added theorem smooth_bump_function.nhds_basis_tsupport

added theorem smooth_bump_function.tsupport_mem_nhds

added theorem smooth_bump_function.tsupport_subset_chart_at_source

added theorem smooth_bump_function.tsupport_subset_ext_chart_at_source

added theorem smooth_bump_function.tsupport_subset_symm_image_closed_ball

Modified src/geometry/manifold/partition_of_unity.lean

Modified src/geometry/manifold/times_cont_mdiff.lean

Modified src/measure_theory/integral/integrable_on.lean

deleted theorem continuous.integrable_of_compact_closure_support

added theorem continuous.integrable_of_has_compact_support

Modified src/topology/algebra/order/compact.lean

added theorem continuous.bdd_above_range_of_has_compact_mul_support

added theorem continuous.bdd_below_range_of_has_compact_mul_support

added theorem continuous.exists_forall_ge'

added theorem continuous.exists_forall_ge_of_has_compact_mul_support

added theorem continuous.exists_forall_le'

modified theorem continuous.exists_forall_le

added theorem continuous.exists_forall_le_of_has_compact_mul_support

added theorem is_compact.bdd_above_image

added theorem is_compact.bdd_below_image

Modified src/topology/homeomorph.lean

added theorem has_compact_mul_support.comp_homeomorph

Modified src/topology/partition_of_unity.lean

Created src/topology/support.lean

added theorem exists_compact_iff_has_compact_mul_support

added theorem has_compact_mul_support.comp_closed_embedding

added theorem has_compact_mul_support.comp_left

added theorem has_compact_mul_support.comp₂_left

added theorem has_compact_mul_support.intro

added theorem has_compact_mul_support.is_compact

added theorem has_compact_mul_support.mono'

added theorem has_compact_mul_support.mono

added theorem has_compact_mul_support.mul

added def has_compact_mul_support

added theorem has_compact_mul_support_comp_left

added theorem has_compact_mul_support_def

added theorem has_compact_mul_support_iff_eventually_eq

added theorem has_compact_support.mul_left

added theorem has_compact_support.mul_right

added theorem has_compact_support.smul_left'

added theorem has_compact_support.smul_left

added theorem has_compact_support.smul_right

added theorem image_eq_zero_of_nmem_mul_tsupport

added theorem is_closed_mul_tsupport

added def mul_tsupport

added theorem mul_tsupport_eq_empty_iff

added theorem not_mem_closure_mul_support_iff_eventually_eq

added theorem subset_mul_tsupport