Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-16 18:01 e7440330

View on Github →

feat(data/finset/basic, lattice): Simple lemmas (#9723) This proves lemmas about finset.sup/finset.inf and finset.singleton.

Estimated changes

added theorem finset.inf_attach
added theorem finset.inf_erase_top
modified theorem finset.inf_image
added theorem finset.inf_inf
added theorem finset.inf_sdiff_left
added theorem finset.inf_sdiff_right
added theorem finset.sup_attach
added theorem finset.sup_erase_bot
modified theorem finset.sup_image
added theorem finset.sup_sdiff_left
added theorem finset.sup_sdiff_right
added theorem finset.sup_singleton'
added theorem finset.sup_sup
added theorem inf_inf_inf_comm
added theorem sup_sup_sup_comm