lattice): add `comp_sup'_eq_sup'_comp`, golf some proofs (#7275)

Commit

4 years ago

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`.

Author

eric-wieser

Parents

9b8d6e49

mathlib 80028f3a - feat(data/finset/lattice): add `comp_sup'_eq_sup'_comp`, golf some proofs (#7275)

mathlib
80028f3a - feat(data/finset/lattice): add `comp_sup'_eq_sup'_comp`, golf some proofs (#7275)