Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-08 05:24 d34b3306

View on Github →

feat(data/set/basic,order/filter/basic): add semiconj lemmas about images and maps (#14970) This adds function.commute and function.semiconj lemmas, and replaces all the uses of _comm lemmas with the semiconj version as it turns out that only this generality is needed.

Estimated changes

Modified src/data/finset/basic.lean

added theorem function.commute.finset_image

added theorem function.commute.finset_map

added theorem function.semiconj.finset_image

added theorem function.semiconj.finset_map

Modified src/data/finset/pointwise.lean

Modified src/data/set/basic.lean

added theorem function.commute.set_image

added theorem function.semiconj.set_image

Modified src/data/set/pointwise.lean

modified theorem set.image_op_inv

Modified src/order/filter/basic.lean

added theorem commute.filter_comap

added theorem commute.filter_map

added theorem function.semiconj.filter_comap

added theorem function.semiconj.filter_map

Modified src/order/filter/pointwise.lean

modified theorem filter.map_inv'

Modified src/topology/algebra/field.lean