Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-07 06:34 ec6f5d16

View on Github →

feat(data/*set): some finite sets lemmas (#7037)

Estimated changes

Modified src/data/finset/basic.lean

added theorem finset.exists_mem_subset_of_subset_bUnion_of_directed_on

Modified src/data/set/finite.lean

added theorem set.finite.fin_embedding

added theorem set.finite.fin_param

Modified src/logic/embedding.lean

added def equiv.as_embedding

added theorem equiv.as_embedding_range