Zulip Chat Archive

Stream: general

Topic: finite intersection


Patrick Massot (Apr 07 2020 at 19:19):

Why is library_search not finding

lemma finite_inter {α : Type*} {s t : set α} (hs : finite s) (ht : finite t) : finite (s  t)

What's wrong with this lemma?

Patrick Massot (Apr 07 2020 at 19:20):

I don't understand how I can have the import defining finite without having this.

Yury G. Kudryashov (Apr 07 2020 at 19:30):

You don't need one of the finite assumptions.

Patrick Massot (Apr 07 2020 at 19:30):

Good point.

Patrick Massot (Apr 07 2020 at 19:30):

I still need a lemma.

Yury G. Kudryashov (Apr 07 2020 at 19:31):

We have finite_subset.

Yury G. Kudryashov (Apr 07 2020 at 19:31):

I think that it should be renamed to finite.subset, and there should be finite.inter_left and finite.inter_right.


Last updated: Dec 20 2023 at 11:08 UTC