isRight_congr — Mathlib

English

If two sum elements are related by LiftRel, then their left components are related in the corresponding domain.

Русский

Если два элемента суммы связаны отношением LiftRel, то их левая часть связана соответствующим образом.

LaTeX

$$$$ \\text{If } \\operatorname{LiftRel}(r,s)\\ x\\ y, \\; x.isLeft \\Rightarrow y.isLeft. $$$$

Lean4

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

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