Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-10 14:02 37c27774

View on Github →

feat(order/filter/ultrafilter): pure, map, and comap lemmas (#15187) A handful of simple lemmas.

Estimated changes

modified theorem ultrafilter.coe_comap
added theorem ultrafilter.coe_pure
added theorem ultrafilter.comap_id
added theorem ultrafilter.comap_pure
added theorem ultrafilter.map_id'
added theorem ultrafilter.map_id
added theorem ultrafilter.map_map
added theorem ultrafilter.map_pure