mk

Mathlib.Testing.Plausible.Functions

URI: https://scilib.ai/kg/mathlib#Plausible.InjectiveFunction.mk

Lean4

/-- Create an injective function from one list and a permutation of that list. -/
protected def mk (xs ys : List α) (h : xs ~ ys) (h' : ys.Nodup) : InjectiveFunction α :=
  have h₀ : xs.length ≤ ys.length := le_of_eq h.length_eq
  have h₁ : ys.length ≤ xs.length := le_of_eq h.length_eq.symm
  InjectiveFunction.mapToSelf (List.toFinmap' (xs.zip ys))
    (by simp only [List.toFinmap', comp_def, List.map_fst_zip, List.map_snd_zip, *, List.map_map])
    (by simp only [List.toFinmap', comp_def, List.map_snd_zip, *, List.map_map])

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru