hom_ext_iff' — Mathlib

English

A variant of hom_ext_iff using explicit sigma-indexed witnesses.

Русский

Вариант утверждения hom_ext_iff с явными свидетелями по сигмаспецификации.

LaTeX

$$$f=g \\iff \\forall i, \\exists h_1: f.f i=g.f i, f.φ_i ≫ eqToHom (by rw [h_1]) = g.φ_i$$$

Lean4

theorem hom_ext_iff' {X Y : FormalCoproduct.{w} C} (f g : X ⟶ Y) :
    f = g ↔ ∀ i : X.I, ∃ h₁ : f.f i = g.f i, f.φ i ≫ eqToHom (by rw [h₁]) = g.φ i :=
  ⟨(· ▸ by simp), fun h ↦ hom_ext (funext fun i ↦ (h i).fst) fun i ↦ (h i).snd⟩

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