orElse_think

Mathlib.Data.Seq.Computation

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

← MathLib Explorer

English

think c₁ <|> think c₂ equals think (c₁ <|> c₂).

Русский

think c₁ <|> think c₂ эквивалентно think (c₁ <|> c₂).

LaTeX

$$$\operatorname{think} c_1 \ <|> \ \operatorname{think} c_2 = \operatorname{think}(c_1 \<|> c_2)$$$

Lean4

@[simp]
theorem orElse_think (c₁ c₂ : Computation α) : (think c₁ <|> think c₂) = think (c₁ <|> c₂) :=
  destruct_eq_think <| by
    unfold_projs
    simp [orElse]

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

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

Разделы

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

Аффилиация

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