exists_of_isRight_left — Mathlib

English

If LiftRel holds for x on the right but y is on the left, there exist witnesses on the right side.

Русский

Если LiftRel связывает x справа и y слева, существуют свидетельства в правой части.

LaTeX

$$$$ \\exists b\\; \\exists d: s b d \\land x = \\mathrm{inr} b \\land y = \\mathrm{inr} d. $$$$

Lean4

theorem exists_of_isRight_left (h₁ : LiftRel r s x y) (h₂ : x.isRight) : ∃ b d, s b d ∧ x = inr b ∧ y = inr d :=
  by
  rcases isRight_iff.mp h₂ with ⟨_, rfl⟩
  simp only [liftRel_iff, false_and, and_false, exists_false, false_or, reduceCtorEq] at h₁
  exact h₁

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