list_flatMap

Mathlib.Computability.Primrec

URI: https://scilib.ai/kg/mathlib#Primrec.list_flatMap

← MathLib Explorer

English

FlatMap, combining map and flatten, is primitive recursive.

Русский

FlatMap, совмещающий map и flatten, примитивно вычислим.

LaTeX

$$$\\mathrm{Primrec}\\left( a \\mapsto (f(a)).\\mathrm{flatMap}(g(a)) \\right)$$$

Lean4

theorem list_flatMap {f : α → List β} {g : α → β → List σ} (hf : Primrec f) (hg : Primrec₂ g) :
    Primrec (fun a => (f a).flatMap (g a)) :=
  list_flatten.comp (list_map hf hg)

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

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

Разделы

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

Аффилиация

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