corecF_eq — Mathlib

English

For any g and x, the destination of corecF g x equals the map of corecF g applied to the representation of g x.

Русский

Для любой g и x пункт назначения corecF g x равняется отображению corecF g на представлении g x.

LaTeX

$$$$\forall {F : Type u \to Type u} [q : QPF F] {\alpha : Type u} (g : \alpha \to F \alpha) (x : \alpha) : PFunctor.M.dest (corecF g x) = q.P.map (corecF g) (repr (g x)).$$$$

Lean4

theorem corecF_eq {α : Type _} (g : α → F α) (x : α) : PFunctor.M.dest (corecF g x) = q.P.map (corecF g) (repr (g x)) :=
  by
  rw [corecF, PFunctor.M.dest_corec]
    -- Equivalence

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