id_sequence

Mathlib.Control.Traversable.Lemmas

URI: https://scilib.ai/kg/mathlib#Traversable.id_sequence

Lean4

theorem id_sequence (x : t α) : sequence (f := Id) (pure <$> x) = pure x := by
  simp [sequence, traverse_map, id_traverse]

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

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

Разделы

Аффилиация

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