injection and surjection

Stream: new members

[Alex Zhang]

Is there a subtype version for https://leanprover-community.github.io/mathlib_docs/data/set/function.html#set.inj_on?

[Eric Wieser]

Can you elaborate on what you mean by that?

[Eric Wieser]

Perhaps give an example of the sort of statement you're looking for?

[Alex Zhang]

Yeah. set.inj_on is def set.inj_on {α : Type u} {β : Type v} (f : α → β) (s : set α) : Prop meaning f is injective on s if the restriction of f to s is injective. Something like subtype.inj_onis jsut changing (s : set α) to s being a subtype of α.

[Eric Wieser]

Can you write out what you want instead of src#set.inj_on?

[Eric Wieser]

Which is

def inj_on (f : α → β) (s : set α) : Prop :=
∀ ⦃x₁ : α⦄, x₁ ∈ s → ∀ ⦃x₂ : α⦄, x₂ ∈ s → f x₁ = f x₂ → x₁ = x₂

[Eric Wieser]

You might be after function.injective (f ∘ (coe : subtype p → α))

[Alex Zhang]

I was not thinking a precise def as I am looking for if there is anything already. The last one you gave seems to be a suggestion for the purpose I described.

[Eric Wieser]

It usually helps to give a precise def even if you're hoping it already exists

[Eric Wieser]

For one, that means you can use library_search to look for the def

[Kevin Buzzard]

Basically Eric is asking you to ask a precise question by writing some lean down