isLeft_left

Mathlib.Data.Sum.Basic

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

English

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

Русский

Если LiftRel связывает x и y и x лежит слева, то найдутся 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_left (h : LiftRel r s x (inl c)) : x.isLeft := by cases h; rfl

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

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

Разделы

Аффилиация

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