Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-11-29 07:22 8e74c62a

View on Github →

chore(data/finset,order/filter): simplify a few proofs (#1747) Also add finset.image_mono and finset.range_mono.

Estimated changes

Modified src/data/finset.lean

added theorem finset.image_mono

added theorem finset.range_mono

added theorem finset.subset_range_sup_succ

Modified src/order/filter/basic.lean