Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-13 02:53 c53285a8

View on Github →

feat(order/filter/lift): drop an unneeded assumption (#14117) Drop monotone _ assumptions in filter.comap_lift_eq and filter.comap_lift'_eq.

Estimated changes

Modified src/order/filter/lift.lean

modified theorem filter.comap_lift'_eq

modified theorem filter.comap_lift_eq

Modified src/order/filter/small_sets.lean

Modified src/topology/uniform_space/basic.lean

Modified src/topology/uniform_space/completion.lean

Modified src/topology/uniform_space/uniform_embedding.lean