results_thinkN_pure

Mathlib.Data.Seq.Computation

URI: https://scilib.ai/kg/mathlib#Computation.results_thinkN_pure

← MathLib Explorer

English

For any a and n, Results (thinkN (pure a) n) a n.

Русский

Пусть a — элемент типа, и n натуральное. Тогда Results (thinkN (pure a) n) a n.

LaTeX

$$$$ \operatorname{Results}(\mathrm{thinkN}(\mathrm{pure} a)\,n)\ a\ n. $$$$

Lean4

theorem results_thinkN_pure (a : α) (n) : Results (thinkN (pure a) n) a n := by
  have := results_thinkN n (results_pure a); rwa [Nat.zero_add] at this

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

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

Разделы

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

Аффилиация

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