Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-03-02 18:11 8919541a

View on Github →

feat(data/finset): new basic material on finsets and fintypes (#2068)

feat(data/finset): additional basic material
minor fixes
golfed
Update src/data/finset.lean Co-Authored-By: Johan Commelin johan@commelin.net
Update src/data/finset.lean Co-Authored-By: Johan Commelin johan@commelin.net
Update src/data/finset.lean Co-Authored-By: Johan Commelin johan@commelin.net
golfed

Estimated changes

Modified src/data/finset.lean

modified theorem finset.le_max'

modified theorem finset.le_min'

added theorem finset.left_eq_union_iff_subset

modified def finset.max'

modified theorem finset.max'_le

modified theorem finset.max'_mem

modified def finset.min'

modified theorem finset.min'_le

modified theorem finset.min'_lt_max'

modified theorem finset.min'_mem

added theorem finset.pi_disjoint_of_disjoint

added theorem finset.pi_subset

added theorem finset.right_eq_union_iff_subset

added theorem finset.sdiff_subset

added theorem finset.singleton_subset_iff

added theorem finset.union_eq_left_iff_subset

added theorem finset.union_eq_right_iff_subset

Modified src/data/fintype.lean

added theorem finset.card_le_one_iff

added theorem finset.one_lt_card_iff

added theorem fintype.mem_pi_finset

added def fintype.pi_finset

added theorem fintype.pi_finset_disjoint_of_disjoint

added theorem fintype.pi_finset_subset

added theorem fintype.pi_finset_univ

Modified src/data/fintype/card.lean

added theorem fintype.card_pi_finset

Modified src/measure_theory/integration.lean