liftRel_cons

Mathlib.Data.WSeq.Relation

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

← MathLib Explorer

English

LiftRel R (cons a s) (cons b t) is equivalent to R a b and LiftRel R s t.

Русский

LiftRel R (cons a s) (cons b t) эквивалентно R a b и LiftRel R s t.

LaTeX

$$$\mathrm{LiftRel}\ R\ (\mathrm{cons}\ a\ s)\ (\mathrm{cons}\ b\ t) \iff (R\ a\ b) \land \mathrm{LiftRel}\ R\ s\ t$$$

Lean4

@[simp]
theorem liftRel_cons (R : α → β → Prop) (a b s t) : LiftRel R (cons a s) (cons b t) ↔ R a b ∧ LiftRel R s t := by
  simp [liftRel_destruct_iff]

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

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

Разделы

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

Аффилиация

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