## Stream: new members

### Topic: subtypes / restrictions

#### Antoine Chambert-Loir (Nov 30 2021 at 09:52):

I tried to find a proof that a restriction of an injective map is injective by library_search but didn't succeed.

example (α β : Type*) (f : α → β) (hf : function.injective f) (s : set α) :
function.injective (set.restrict f s) :=
begin
intros a b h,
apply subtype.ext_val,
apply hf,
exact h,
end


By the way, I wonder, in the situation of a map fin n.succ \to \alpha how one should get its restriction to fin n.
Maybe it is better to do just by composition with fin.cast_le (nat.le_succ n) (it saves a quantifier).

#### Johan Commelin (Nov 30 2021 at 09:53):

I would certainly use the composition

#### Antoine Chambert-Loir (Nov 30 2021 at 10:08):

Johan Commelin said:

I would certainly use the composition

Which means, by the way, that good writing in Lean probably requires thinking categorically.

#### Johan Commelin (Nov 30 2021 at 10:09):

@Antoine Chambert-Loir There's certainly a tendency towards that. Type theory nudges you in that direction.

#### Anatole Dedecker (Nov 30 2021 at 10:16):

I’m curious : does hf.comp subtype.coe_injective work as a proof of your example ?

#### Antoine Chambert-Loir (Nov 30 2021 at 10:25):

Anatole Dedecker said:

I’m curious : does hf.comp subtype.coe_injective work as a proof of your example ?

Yes !

#### Anatole Dedecker (Nov 30 2021 at 10:56):

So in fact set.restrict is already the composition with coe

#### Antoine Chambert-Loir (Nov 30 2021 at 11:16):

I see. In fact, to propose a mwe, I had simplified my own stuff where s was a set.range of an injective map (nat.cast_le _), hence the simplification. As Johan wrote, it is probably better to compose explicitly with coe in my case.

Last updated: Dec 20 2023 at 11:08 UTC