liftRelAux_inr_inr

Mathlib.Data.Seq.Computation

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

English

Simplicity variant of ret_left restated in a simp lemma.

Русский

Упрощённая версия ret_left как лемма simp.

LaTeX

$$$(simp variant of ret_left)$$$

Lean4

@[simp]
theorem liftRelAux_inr_inr {ca cb} : LiftRelAux R C (Sum.inr ca) (Sum.inr cb) = C ca cb :=
  rfl

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

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

Разделы

Аффилиация

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