ext_from_iff — Mathlib

English

An equivalence: f=g if and only if their inl- and inr-based compositions coincide.

Русский

Эквиваленция: f=g, если и только если совпадают композиции через inl φ и через inr φ.

LaTeX

$$$\forall i,j:\ hij: j+1=i:\ f,g:(mappingCone φ)X_j\to A:\ (f=g)\iff\ ((inl φ)_{i,j}∘f)=(inl φ)_{i,j}∘g\land\ ((inr φ)_{j}∘f)=(inr φ)_{j}∘g.$$$

Lean4

theorem ext_from_iff (i j : ℤ) (hij : j + 1 = i) {A : C} (f g : (mappingCone φ).X j ⟶ A) :
    f = g ↔ (inl φ).v i j (by cutsat) ≫ f = (inl φ).v i j (by cutsat) ≫ g ∧ (inr φ).f j ≫ f = (inr φ).f j ≫ g :=
  by
  constructor
  · rintro rfl
    tauto
  · rintro ⟨h₁, h₂⟩
    exact ext_from φ i j hij h₁ h₂

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