Finset.InjOn.map

Stream: Is there code for X?

[Antoine Chambert-Loir]

to define maps of Finset under a Function, mathlib has Finset.map when the map is an embedding, and Finset.image in general, given a decidability instance. The case where the map is injective on the given Finset seems to be missing :

def _root_.Finset.InjOn.map {α β : Type*} {f : α → β}
    (s : Finset α) (hs : Set.InjOn f s) : Finset β  := {
  val := Multiset.map f s.val,
  nodup := (Multiset.nodup_map_iff_inj_on s.nodup).mpr hs }

should I PR it?

[Eric Wieser]

Is there a way to spell this with s.attach.map?

[Ruben Van de Velde]

import Mathlib

theorem extracted_2.{u_1, u_2} {α : Type u_1} {β : Type u_2} {f : α → β} (s : Set α) (hs : Set.InjOn f s) :
    Function.Injective fun (x : s) => f x := fun x y h => SetCoe.ext <| hs x.prop y.prop h

theorem extracted_1.{u_1, u_2} {α : Type u_1} {β : Type u_2} {f : α → β} (s : Finset α) (hs : Set.InjOn f s) :
    Function.Injective fun (x : s) => f x := extracted_2 s hs

def _root_.Finset.InjOn.map {α β : Type*} {f : α → β}
    (s : Finset α) (hs : Set.InjOn f s) : Finset β  :=
  s.attach.map { inj' := extracted_1 s hs }

[Antoine Chambert-Loir]

My version was analogous :

def Set.InjOn.embedding {α β : Type*} {f : α → β}  {s : Finset α} (hs : Set.InjOn f s) :
  s ↪ β := {
    toFun := Set.restrict s f,
    inj' := fun x y h => SetCoe.ext (hs x.prop y.prop h) }

def Finset.map_of_injOn' {α β : Type*} (f : α → β)
    (s : Finset α) (hs : Set.InjOn f s) : Finset β  :=
  s.attach.map (Set.InjOn.embedding hs)

[Antoine Chambert-Loir]

and I guess, Set.InjOn.embedding suffices, without needing to explicitly define the second one.

[Eric Wieser]

import Mathlib

def _root_.Finset.InjOn.map {α β : Type*} {f : α → β}
    (s : Finset α) (hs : Set.InjOn f s) : Finset β  :=
  s.attach.map { inj' := hs.injective }

(docs#Set.InjOn.injective)

[Eric Wieser]

Set.InjOn.embedding seems like a reasonable thing to PR