exists_of_isLeft_left — Mathlib

English

From isLeft-right congruence under LiftRel one can extract left-right witnesses in multiple forms.

Русский

Из условий левостороннего правостороннего соответствия можно извлечь лево-правые свидетельства.

LaTeX

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

Lean4

theorem exists_of_isLeft_left (h₁ : LiftRel r s x y) (h₂ : x.isLeft) : ∃ a c, r a c ∧ x = inl a ∧ y = inl c :=
  by
  rcases isLeft_iff.mp h₂ with ⟨_, rfl⟩
  simp only [liftRel_iff, false_and, and_false, exists_false, or_false, reduceCtorEq] at h₁
  exact h₁

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