## Stream: new members

### Topic: Functional extensionality

#### Ken Roe (Jul 24 2018 at 21:53):

Is there a functionality extensionality theorem like the one shown below in one of the libraries:

theorem fun_ext {t} {u} :
∀ (a:t→u) (b:t→u), a=b → (λ (x:t), a)=(λ (x:t), b) := sorry.


#### Chris Hughes (Jul 24 2018 at 21:56):

There's funext, but that's not the same as what you stated. The proof of the theorem you stated is assume a b h, by rw h

#### Ken Roe (Jul 24 2018 at 22:36):

Thanks. I'm running into another issue. It seems I cannot rewrite if meta variables are involved. How is the following theorem completed (ignore the "admit"--I'd like to get the "rw h" to work.

theorem dd : (λ (x:ℕ), x*2)=(λ (x:ℕ), x+x) := begin
have h:∀ x, x*2=x+x, intro, admit,
rw h
end


#### Simon Hudon (Jul 24 2018 at 22:44):

You can't rewrite bound variables. Use simp only [h] instead

#### Simon Hudon (Jul 24 2018 at 22:45):

Is there a functionality extensionality theorem like the one shown below in one of the libraries:

theorem fun_ext {t} {u} :
∀ (a:t→u) (b:t→u), a=b → (λ (x:t), a)=(λ (x:t), b) := sorry


Isn't that normal rewriting?

Last updated: May 08 2021 at 19:11 UTC