mathlib3
9b4f0cf8 - feat(data/basic/lean): add lemmas finset.subset_iff_inter_eq_{left, right} (#7053)

Commit
4 years ago
feat(data/basic/lean): add lemmas finset.subset_iff_inter_eq_{left, right} (#7053) These lemmas are the analogues of `set.subset_iff_inter_eq_{left, right}`, except stated for `finset`s. Zulip: https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/finset.2Esubset_iff_inter_eq_left.20.2F.20right Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Author
Parents
Loading