lambda abstraction

Stream: new members

[bumby bumby]

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

[Hanting Zhang]

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

[Yakov Pechersky]

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.

[Yakov Pechersky]

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

[Yakov Pechersky]

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.