exists_of_isLeft_right — Mathlib

English

Another formulation of the left-right existential property under LiftRel.

Русский

Еще одно формулирование существования слева справа в рамках LiftRel.

LaTeX

$$$$ \\exists a,c: r a c \\land x = \\mathrm{inl} a \\land y = \\mathrm{inl} c. $$$$

Lean4

theorem exists_of_isLeft_right (h₁ : LiftRel r s x y) (h₂ : y.isLeft) : ∃ a c, r a c ∧ x = inl a ∧ y = inl c :=
  exists_of_isLeft_left h₁ ((isLeft_congr h₁).mpr h₂)

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