Commit 2023-02-02 07:44 3914ed58

View on Github →

feat: port Topology.Support (#2002)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Support.lean

added theorem HasCompactMulSupport.comp_closedEmbedding

added theorem HasCompactMulSupport.comp_left

added theorem HasCompactMulSupport.comp₂_left

added theorem HasCompactMulSupport.intro

added theorem HasCompactMulSupport.isCompact

added theorem HasCompactMulSupport.isCompact_range

added theorem HasCompactMulSupport.mono'

added theorem HasCompactMulSupport.mono

added theorem HasCompactMulSupport.mul

added def HasCompactMulSupport

added theorem HasCompactSupport.mul_left

added theorem HasCompactSupport.mul_right

added theorem HasCompactSupport.smul_left'

added theorem HasCompactSupport.smul_left

added theorem HasCompactSupport.smul_right

added theorem LocallyFinite.exists_finset_nhd_mulSupport_subset

added theorem continuous_of_mulTSupport

added theorem exists_compact_iff_hasCompactMulSupport

added theorem hasCompactMulSupport_comp_left

added theorem hasCompactMulSupport_def

added theorem hasCompactMulSupport_iff_eventuallyEq

added theorem image_eq_one_of_nmem_mulTSupport

added theorem isClosed_mulTSupport

added def mulTSupport

added theorem mulTSupport_eq_empty_iff

added theorem not_mem_mulTSupport_iff_eventuallyEq

added theorem range_eq_image_mulTSupport_or

added theorem range_subset_insert_image_mulTSupport

added theorem subset_mulTSupport

added theorem tsupport_mul_subset_left

added theorem tsupport_mul_subset_right

added theorem tsupport_smul_subset_left