Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-08 15:56 bcf5b1a6

View on Github →

feat(data/fintype/basic): to_finset lattice lemmas (#7077) While we do not have lattice homomorphisms, we can still provide some similar API.

Estimated changes

Modified src/data/fintype/basic.lean

added theorem set.to_finset_disjoint_iff

added theorem set.to_finset_mono

added theorem set.to_finset_strict_mono

Modified src/data/set/finite.lean

added theorem set.finite.diff

added theorem set.finite.to_finset_inj

added theorem set.finite.to_finset_mono

added theorem set.finite.to_finset_strict_mono

added theorem set.finite.union_iff

added theorem set.finite_to_finset_eq_empty_iff

added theorem set.insert_to_finset