Commit 2023-05-14 07:54 d0773f91

View on Github →

feat: finset distributivity lemmas (#3937) Match https://github.com/leanprover-community/mathlib/pull/18611 data.finset.lattice@9d684a893c52e1d6692a504a118bfccbae04feeb..2d44d6823a96f9c79b7d1ab185918377be663424

Estimated changes

deleted theorem Finset.inf_eq_top_iff
added theorem Finset.inf_himp_right
added theorem Finset.inf_sup
added theorem Finset.inf_sup_inf
deleted theorem Finset.sup_eq_bot_iff
added theorem Finset.sup_himp_left
added theorem Finset.sup_himp_right
added theorem Finset.sup_inf
added theorem Finset.sup_inf_sup