maps_to_prod

Stream: Is there code for X?

[Chris Birkbeck]

Do we have the following:

lemma maps_to_prod_fst  {α : Type*} {β : Type*}
(s : set α) (v : set β): maps_to prod.fst (s ×ˢ v) s :=
begin
sorry,
end

I can't seem to find it, but it feels like it should be somewhere.

[Yaël Dillies]

I don't remember seeing it, but the proof is something like λ _, and.left.

[Chris Birkbeck]

Well thats a nice short proof.