liftRelAux_inl_inl

Mathlib.Data.Seq.Computation

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

English

Second copy of LiftRel Bind statement for completeness.

Русский

Вторая копия утверждения LiftRel Bind для полноты.

LaTeX

$$$\\text{LiftRel }S (s1\\ f1) (s2\\ f2)$$$

Lean4

@[simp]
theorem liftRelAux_inl_inl {a : α} {b : β} : LiftRelAux R C (Sum.inl a) (Sum.inl b) = R a b :=
  rfl

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

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

Разделы

Аффилиация

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