Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-26 12:23 d2b12217

View on Github →

feat(algebra/order/group|order/filter): add two lemmas (#9956)

  • Also open function namespace in order.filter.basic
  • From the sphere eversion project

Estimated changes

added theorem le_div_self_iff
modified theorem filter.comap_map
modified theorem filter.image_mem_map_iff
modified theorem filter.map_inf
modified theorem filter.map_inj
modified theorem filter.mem_comap_iff
modified theorem filter.pure_injective