inl_eq_inr_iff — Mathlib

English

In a pushout, inl x1 = inr x2 iff there exists s with f s = x1 and g s = x2.

Русский

В пушоуте inl x1 = inr x2 эквивалентно существованию s с f s = x1 и g s = x2.

LaTeX

$$inl f g x1 = inr f g x2 ↔ ∃ s, f s = x1 ∧ g s = x2$$

Lean4

theorem inl_eq_inr_iff [Mono f] (x₁ : X₁) (x₂ : X₂) : (inl f g x₁ = inr f g x₂) ↔ ∃ (s : S), f s = x₁ ∧ g s = x₂ :=
  by
  refine (Pushout.quot_mk_eq_iff f g (Sum.inl x₁) (Sum.inr x₂)).trans ?_
  constructor
  · rintro ⟨⟩
    exact ⟨_, rfl, rfl⟩
  · rintro ⟨s, rfl, rfl⟩
    apply Rel'.inl_inr

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