Commit 2026-07-14 11:01 7fff4171

View on Github →

feat(Topology/Algebra/Group/Basic,Algebra/Group/Pointwise/Set/Basic): add Filter.map_{sub,div}{Left,Right}_nhds{,LT,GT,NE} (#41376) The file Topology/Algebra/Group/Basic contains various variants of Filter.map_mulLeft_nhds and Filter.map_mulRight_nhds. The PR adds the analogous lemmas for division, with very similar proofs (which requires adding some helper lemmas to Algebra/Group/Pointwise/Set/Basic). Using `to_additive', one also obtains lemmas for subtraction for free,

Estimated changes

Modified Mathlib/Algebra/Group/Pointwise/Set/Basic.lean

added theorem Set.image_div_left

added theorem Set.image_div_right

added theorem Set.preimage_inv_mul_right_singleton

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

modified theorem Filter.inv_nhdsGT

modified theorem Filter.inv_nhdsLT

modified theorem Filter.inv_nhdsNE

added theorem Filter.map_divLeft_nhds

added theorem Filter.map_divLeft_nhdsGT

added theorem Filter.map_divLeft_nhdsLT

added theorem Filter.map_divLeft_nhdsNE

added theorem Filter.map_divRight_nhds

added theorem Filter.map_divRight_nhdsGT

added theorem Filter.map_divRight_nhdsLT

added theorem Filter.map_divRight_nhdsNE

modified theorem Filter.map_mul_left_nhdsGT

modified theorem Filter.map_mul_left_nhdsLT

modified theorem Filter.map_mul_right_nhdsGT

modified theorem Filter.map_mul_right_nhdsLT

added theorem Homeomorph.coe_divLeft

added theorem Homeomorph.coe_divRight