fin zip function

Stream: new members

[Patrick Thomas]

Is there a way to fix this?

example
  {α β : Type} [decidable_eq α]
  {n : ℕ}
  (f : fin n → α)
  (g : fin n → β)
  (default : α → β) :
  α → β :=
fun x : α, if h : ∃ m : fin n, f m = x then g m else default x

[Patrick Thomas]

Or do something similar?

[Kevin Buzzard]

What if there are two different m's with f(m)=x?

[Eric Wieser]

I think you want docs#nat.find to extract the m from the h

[Patrick Thomas]

Kevin Buzzard said:

What if there are two different m's with f(m)=x?

Yes, that is a good point. I should have added the condition that there are not.

[Eric Wieser]

docs#fintype.choose would also work if you add that condition

[Patrick Thomas]

Thank you!