mapIdxM'_eq_mapIdxM

Mathlib.Data.List.Indexes

URI: https://scilib.ai/kg/mathlib#List.mapIdxM'_eq_mapIdxM

← MathLib Explorer

English

A monadic variant of mapIdxM' equals mapIdxM, up to a unit value.

Русский

Моноидальная версия mapIdxM' равна mapIdxM с добавлением единицы.

LaTeX

$$$$ \mathrm{mapIdxM'}\ f\ as = \mathrm{mapIdxM}\ f\ as \; *> \; \mathrm{pure}\ PUnit.\,unit. $$$$

Lean4

theorem mapIdxM'_eq_mapIdxM {α} (f : ℕ → α → m PUnit) (as : List α) : mapIdxM' f as = mapIdxM f as *> pure PUnit.unit :=
  mapIdxMAux'_eq_mapIdxMGo f as #[]

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

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

Разделы

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

Аффилиация

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