liftRel_nil

Mathlib.Data.WSeq.Relation

URI: https://scilib.ai/kg/mathlib#Stream'.WSeq.liftRel_nil

English

LiftRel R nil nil holds for any R.

Русский

LiftRel R nil nil верно для любого R.

LaTeX

$$$\mathrm{LiftRel} R\, \mathrm{nil}\, \mathrm{nil}$$$

Lean4

@[simp]
theorem liftRel_nil (R : α → β → Prop) : LiftRel R nil nil := by simp [liftRel_destruct_iff]

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

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

Разделы

Аффилиация

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