Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-18 11:39 24792be6

View on Github →

chore(data/finset): minor review (#3105)

Estimated changes

Modified src/analysis/convex/basic.lean

Modified src/data/equiv/basic.lean

modified theorem equiv.nonempty_iff_nonempty

Modified src/data/finset.lean

modified theorem finset.coe_erase

modified theorem finset.coe_filter

modified theorem finset.coe_image

modified theorem finset.coe_insert

modified theorem finset.coe_map

modified theorem finset.coe_nonempty

modified theorem finset.coe_sdiff

modified theorem finset.coe_ssubset

modified theorem finset.coe_subset

modified theorem finset.comp_inf_eq_inf_comp

deleted theorem finset.lt_inf

added theorem finset.lt_inf_iff

modified theorem finset.ssubset_iff

Modified src/data/multiset.lean

added theorem multiset.ndinter_subset_left

added theorem multiset.subset_ndunion_right

Modified src/data/set/basic.lean

added theorem set.ssubset_iff_insert

Modified src/data/set/lattice.lean

added theorem set.bot_eq_empty

added theorem set.inf_eq_inter

added theorem set.le_eq_subset

added theorem set.lt_eq_ssubset

added theorem set.sup_eq_union

Modified src/logic/function/basic.lean

modified def function.injective.decidable_eq

Modified src/order/basic.lean

deleted theorem monotone.order_dual

Modified src/order/lattice.lean

added theorem monotone.map_inf

added theorem monotone.map_sup