inl_rel'_inl_iff — Mathlib

English

In the pushout, the equality of inl x1 and inr x2 corresponds exactly to existence of s in S with f s = x1 and g s = x2.

Русский

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

LaTeX

$$Eq (Pushout.inl f g x1) (Pushout.inr f g x2) ↔ ∃ s, f s = x1 ∧ g s = x2$$

Lean4

@[simp]
theorem inl_rel'_inl_iff (x₁ y₁ : X₁) :
    Rel' f g (Sum.inl x₁) (Sum.inl y₁) ↔ x₁ = y₁ ∨ ∃ (x₀ y₀ : S) (_ : g x₀ = g y₀), x₁ = f x₀ ∧ y₁ = f y₀ :=
  by
  constructor
  · rintro (_ | ⟨_, _, h⟩)
    · exact Or.inl rfl
    · exact Or.inr ⟨_, _, h, rfl, rfl⟩
  · rintro (rfl | ⟨_, _, h, rfl, rfl⟩)
    · apply Rel'.refl
    · exact Rel'.inl_inl _ _ h

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