Commit 2021-04-21 09:38 80028f3a
View on Github →feat(data/finset/lattice): add comp_sup'_eq_sup'_comp, golf some proofs (#7275)
The proof is just a very marginally generalized version of the previous proof for sup'_apply.
feat(data/finset/lattice): add comp_sup'_eq_sup'_comp, golf some proofs (#7275)
The proof is just a very marginally generalized version of the previous proof for sup'_apply.