Mathlib v3 is deprecated. Go to Mathlib v4

Theorem ultrafilter.pure_injective

Modification history

2022-07-10 14:02

src/order/filter/ultrafilter.lean

feat(order/filter/ultrafilter): `pure`, `map`, and `comap` lemmas (#15187) …

Added ultrafilter.pure_injective View on Github →