isLeft_congr

Mathlib.Data.Sum.Basic

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

English

If f and g are injective and their images are disjoint, then Sum.elim f g is injective.

Русский

Если f и g инъективны и их образы не пересекаются, то Sum.elim f g инъективен.

LaTeX

$$$$ \\operatorname{Injective}(\\mathrm{Sum.elim} f g) $$$$

Lean4

theorem isLeft_congr (h : LiftRel r s x y) : x.isLeft ↔ y.isLeft := by cases h <;> rfl

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

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

Разделы

Аффилиация

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