desc_toCocone_desc_app — Mathlib

English

For any f: Quot F →+ A and hc IsColimit of c, and for any x ∈ Quot F, hc.desc (toCocone F f) (Quot.desc F c x) = f x.

Русский

Для любого f: Quot F →+ A и hc IsColimit c и любого x ∈ Quot F, выполняется hc.desc (toCocone F f) (Quot.desc F c x) = f x.

LaTeX

$$$ hc.desc (toCocone F f) (Quot.desc F c x) = f x $$$

Lean4

theorem desc_toCocone_desc_app [DecidableEq J] {A : Type w} [AddCommGroup A] (f : Quot F →+ A) (hc : IsColimit c)
    (x : Quot F) : hc.desc (toCocone F f) (Quot.desc F c x) = f x :=
  by
  conv_rhs => rw [← Quot.desc_toCocone_desc F c f hc]
  dsimp

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