rightInverse_list

Mathlib.Data.W.Constructions

URI: https://scilib.ai/kg/mathlib#WType.rightInverse_list

Lean4

theorem rightInverse_list : Function.RightInverse (ofList γ) (toList _)
  | List.nil => rfl
  | List.cons hd tl => by simp [rightInverse_list tl]

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

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

Разделы

Аффилиация

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