subtypes / restrictions

Stream: new members

[Antoine Chambert-Loir]

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]

I would certainly use the composition

[Eric Wieser]

docs#matrix.vec_tail?

[Antoine Chambert-Loir]

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]

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

[Anatole Dedecker]

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

[Antoine Chambert-Loir]

Anatole Dedecker said:

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

Yes !

[Anatole Dedecker]

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

[Antoine Chambert-Loir]

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.