Zulip Chat Archive

Stream: new members

Topic: lambda abstraction

view this post on Zulip bumby bumby (Apr 16 2021 at 17:06):

hi, i m trying to understand the next proof about injective functions and compositions. In general i understood it. Most my problem is that i dont understand the notation or sintax specially lines 10 and 11 exactly the letter "h", i read it seems like lambda abstractions. someone can explain me what are those "h" and what is an equivalence when write the same proof but in paper with pencil and erraser? imagen.png

view this post on Zulip Hanting Zhang (Apr 16 2021 at 17:17):

hf : injective f is a proof that f is injective. Also, please try to use #backticks and follow #mwe guidelines when posting code

view this post on Zulip Yakov Pechersky (Apr 16 2021 at 17:17):

There is nothing special about the letter h. We're just saying that not only do we have a function from X to Y that we call f, we also say that we have a hypothesis that this function f is injective, or the property injective f. We are calling this hypothesis hf, like a variable name.

view this post on Zulip Yakov Pechersky (Apr 16 2021 at 17:18):

The real magic is on lines 21 and 23, where the definition of injective is used.

view this post on Zulip Yakov Pechersky (Apr 16 2021 at 17:20):

We use the hypothesis that injective f to change our goal, on line 21. The hypothesis states that if f a = f b then a = b. And our goal was a = b, so it would be enough to prove f a = f b and then say, by the injectivity of f, a = b. So we can work backwards, saying, I need to prove a = b. I also know that injective f, by the hypothesis I called hf. So I can apply that hypothesis, leaving me to prove f a = f b.

Last updated: May 17 2021 at 21:12 UTC