inl_rel'_inr_iff — Mathlib

English

If an element is in the left injection and the right injection of the pushout, then it exactly comes from some s ∈ S with x1=f s and x2=g s.

Русский

Если элемент лежит в левой инъекции и правой инъекции пушоута, то он точно восходит к некоторому s ∈ S с x1=f s и x2=g s.

LaTeX

$$$\\forall x_1,x_2, Rel'(f,g) (Sum.inl x_1) (Sum.inr x_2) \\iff \\exists s, x_1=f s ∧ x_2=g s$$$

Lean4

@[simp]
theorem inl_rel'_inr_iff (x₁ : X₁) (x₂ : X₂) : Rel' f g (Sum.inl x₁) (Sum.inr x₂) ↔ ∃ (s : S), x₁ = f s ∧ x₂ = g s :=
  by
  constructor
  · rintro ⟨_⟩
    exact ⟨_, rfl, rfl⟩
  · rintro ⟨s, rfl, rfl⟩
    exact Rel'.inl_inr _

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