Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-07 22:47 8a80759b

View on Github →

feat(order/filter/basic): add map_le_map and map_injective (#15128)

  • Add filter.map_le_map, an iff version of filter.map_mono.
  • Add filter.map_injective, a function.injective version of filter.map_inj.

Estimated changes

modified theorem filter.map_inj
added theorem filter.map_injective
added theorem filter.map_le_map_iff