ext_from_X' — Mathlib

English

If f, g: X φ i → A satisfy inrX φ i ≫ f = inrX φ i ≫ g, then f = g.

Русский

Пусть f, g: X φ i → A удовлетворяют inrX φ i ≫ f = inrX φ i ≫ g, тогда f = g.

LaTeX

$$$ inrX\\,\\phi\\,i \\circ f = inrX\\,\\phi\\,i \\circ g \\Rightarrow f = g. $$$

Lean4

theorem ext_from_X' (i : ι) (hi : ¬c.Rel i (c.next i)) {A : C} {f g : X φ i ⟶ A} (h : inrX φ i ≫ f = inrX φ i ≫ g) :
    f = g := by
  rw [← cancel_epi (XIso φ i hi).inv]
  simpa only [inrX, dif_neg hi] using h

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