isLeft_right

Mathlib.Data.Sum.Basic

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

English

Given LiftRel r s x y and y is left, there exist a,c with x = inl a, y = inl c and r a c.

Русский

Если LiftRel связывает x и y и y лежит слева, найдутся a,c такие, что x=inl(a), y=inl(c) и r a c.

LaTeX

$$$$ \\exists a\\;\\exists c\\; (r\\ a\\ c) \\wedge (x = \\mathrm{inl} a) \\wedge (y = \\mathrm{inl} c). $$$$

Lean4

theorem isLeft_right (h : LiftRel r s (inl a) y) : y.isLeft := by cases h; rfl

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

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

Разделы

Аффилиация

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