Commit 2022-06-27 21:32 f6b728f4

View on Github →

feat(data/finset/pointwise): • and ⊆ (#14968) Port set lemmas to finset. Tag a few more lemmas with norm_cast. Add some missing to_additive attributes.

Estimated changes

Modified src/data/finset/basic.lean

added theorem finset.image_subset_image_iff

Modified src/data/finset/pointwise.lean

modified theorem finset.coe_one

added theorem finset.inv_smul_mem_iff

added theorem finset.inv_smul_mem_iff₀

added theorem finset.mem_inv_smul_finset_iff

added theorem finset.mem_inv_smul_finset_iff₀

modified theorem finset.pairwise_disjoint_smul_iff

added theorem finset.smul_finset_subset_iff

added theorem finset.smul_finset_subset_iff₀

added theorem finset.smul_finset_subset_smul_finset_iff

added theorem finset.smul_finset_subset_smul_finset_iff₀

added theorem finset.smul_finset_univ₀

added theorem finset.smul_mem_smul_finset_iff

added theorem finset.smul_mem_smul_finset_iff₀

added theorem finset.smul_univ₀

added theorem finset.subset_smul_finset_iff

added theorem finset.subset_smul_finset_iff₀

Modified src/data/fintype/basic.lean

modified theorem finset.coe_univ

Modified src/data/set/pointwise.lean

modified theorem set.pairwise_disjoint_smul_iff