list map mem eq injective

Stream: Is there code for X?

[Kayla Thomas]

I think it should be possible to prove this

a2: List.map (openVar k v) xs = List.map (openVar k v) xs'
⊢ xs = xs'

given that

lemma OpenVarCloseVarComp
  (x : Var)
  (v : String)
  (k : ℕ)
  (h1 : Var.lc_at k x) :
  (openVar k v ∘ closeVar k v) x = x

because OpenVarCloseVarComp implies that openVar k v is injective in a sense, but I'm not sure of the best way to show this. Is there a lemma relating injective functions and maps that would help?

[Notification Bot]

This topic was moved here from #Is there code for X? > list map mem eq by Kayla Thomas.

[Ruben Van de Velde]

@loogle List.map, Function.Injective

[loogle]

:search: List.map_diff, List.map_erase, and 7 more

[Ruben Van de Velde]

docs#List.map_injective_iff seems useful

[Kayla Thomas]

Thank you.

[Kayla Thomas]

Are there any definitions/lemmas in mathlib about a function only being injective under conditions on its domain?

[Ruben Van de Velde]

Perhaps docs#Set.InjOn

[Kayla Thomas]

Nice. Thank you.