liftRel_pure

Mathlib.Data.Seq.Computation

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

English

LiftRel R (pure a) (pure b) holds iff R a b.

Русский

LiftRel R (pure a) (pure b) выполняется тогда и только тогда, когда R a b.

LaTeX

$$$\\mathrm{LiftRel}\\,R(\\mathrm{pure}\\ a)(\\mathrm{pure}\\ b) \\ \\leftrightarrow\\ R\\ a\\ b$$$

Lean4

theorem liftRel_pure (R : α → β → Prop) (a : α) (b : β) : LiftRel R (pure a) (pure b) ↔ R a b := by simp

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

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

Разделы

Аффилиация

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