isRight_right

Mathlib.Data.Sum.Basic

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

English

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

Русский

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

LaTeX

$$$$ \\text{(h)} \\; x \\text{ isRight} \\Rightarrow x = \\mathrm{inr}(b). $$$$

Lean4

theorem isRight_right (h : LiftRel r s (inr b) y) : y.isRight := by cases h; rfl

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

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

Разделы

Аффилиация

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