Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-12-06 13:30 f9b39eb1

View on Github →

feature(.): add various theorems

Estimated changes

Modified data/finset.lean

added theorem finset.bind_mono

added theorem finset.bind_singleton

Modified data/prod.lean

added theorem prod.eq_iff_fst_eq_snd_eq

added theorem prod.exists

added theorem prod.forall

modified theorem prod.fst_swap

modified theorem prod.mk.eta

added theorem prod.mk.inj_iff

modified theorem prod.snd_swap

modified def prod.swap

modified theorem prod.swap_left_inverse

modified theorem prod.swap_prod_mk

modified theorem prod.swap_right_inverse

modified theorem prod.swap_swap

modified theorem prod.swap_swap_eq

Modified data/set/basic.lean

added theorem set.diff_diff

added theorem set.insert_sdiff

added theorem set.insert_subset

added theorem set.insert_subset_insert

added theorem set.insert_union

modified theorem set.nonempty_of_inter_nonempty_left

modified theorem set.nonempty_of_inter_nonempty_right

modified theorem set.not_not_mem

added theorem set.not_subset

modified theorem set.ssubset_def

added theorem set.union_insert

Modified data/set/finite.lean

added theorem set.finite.dinduction_on

added theorem set.to_finset_insert

Modified logic/basic.lean

deleted theorem prod.exists

deleted theorem prod.forall

deleted theorem prod.mk.inj_iff