# Zulip Chat Archive

## Stream: new members

### Topic: lambda abstraction

#### 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

#### 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

#### 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.

#### Yakov Pechersky (Apr 16 2021 at 17:18):

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

is used.

#### 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