Commit 2023-11-01 07:43 feebec3b

View on Github →

feat: multiplication by closure {1} in topological groups does not change closed and open subsets (#7858)

Estimated changes

Modified Mathlib/Data/Set/Pointwise/SMul.lean

Modified Mathlib/Topology/Algebra/Group/Basic.lean

added theorem HasCompactSupport.eq_zero_or_locallyCompactSpace_of_group

added theorem IsClosed.mul_closure_one_eq

added theorem IsCompact.locallyCompactSpace_of_mem_nhds_of_group

added theorem IsCompact.mul_closure_one_eq_closure

modified theorem IsOpen.closure_div

modified theorem IsOpen.closure_mul

modified theorem IsOpen.div_closure

modified theorem IsOpen.mul_closure

added theorem IsOpen.mul_closure_one_eq

modified theorem QuotientGroup.isClosedMap_coe

added theorem Subgroup.coe_topologicalClosure_bot

added theorem compl_mul_closure_one_eq

added theorem compl_mul_closure_one_eq_iff

added theorem eq_zero_or_locallyCompactSpace_of_support_subset_isCompact_of_group

added theorem subset_mul_closure_one

Modified Mathlib/Topology/Algebra/MulAction.lean

added theorem IsCompact.smul_set

added theorem smul_set_closure_subset