finite intersection

Stream: general

[Patrick Massot]

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]

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

[Yury G. Kudryashov]

You don't need one of the finite assumptions.

[Patrick Massot]

Good point.

[Patrick Massot]

I still need a lemma.

[Yury G. Kudryashov]

We have finite_subset.

[Yury G. Kudryashov]

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