isRight_left

Mathlib.Data.Sum.Basic

URI: https://scilib.ai/kg/mathlib#Sum.LiftRel.isRight_left

English

If LiftRel holds for x = inr b and y, then y is on the right branch.

Русский

Если LiftRel относится к x = inr b и y, то y лежит в правой ветви.

LaTeX

$$$$ \\text{If } \\mathrm{LiftRel}(r,s)\\,(\\mathrm{inr}\\; b)\\; y, \\; y.isRight. $$$$

Lean4

theorem isRight_left (h : LiftRel r s x (inr d)) : x.isRight := by cases h; rfl

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

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

Разделы

Аффилиация

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