Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-09 22:44 f5fa6149

View on Github →

chore(*): some monotonicity lemmas (#3344)

Estimated changes

Modified src/data/set/lattice.lean

added theorem set.bInter_mono'

added theorem set.bInter_mono

Modified src/order/filter/basic.lean

modified theorem filter.comap_mono

modified theorem filter.map_mono

modified theorem filter.monotone_principal

modified theorem filter.prod_mono

modified theorem filter.seq_mono

Modified src/tactic/monotonicity/lemmas.lean