ext — Mathlib

English

Two morphisms Φ1, Φ2: S1 ⟶ S2 are equal if their f-components agree on all indices. Extensionality principle.

Русский

Две стрелки Φ1, Φ2: S1 → S2 равны, если их компоненты f совпадают на всех индексах.

LaTeX

$$$\forall n, (Φ_1.f)(n) = (Φ_2.f)(n) \Rightarrow Φ_1 = Φ_2$$$

Lean4

@[ext]
theorem ext {S₁ S₂ : Split C} (Φ₁ Φ₂ : Hom S₁ S₂) (h : ∀ n : ℕ, Φ₁.f n = Φ₂.f n) : Φ₁ = Φ₂ :=
  by
  rcases Φ₁ with ⟨F₁, f₁, c₁⟩
  rcases Φ₂ with ⟨F₂, f₂, c₂⟩
  have h' : f₁ = f₂ := by
    ext
    apply h
  subst h'
  simp only [mk.injEq, and_true]
  apply S₁.s.hom_ext
  intro n
  dsimp
  rw [c₁, c₂]

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