cone_π_app_comp_Pi_π_pos — Mathlib

English

For n and m with n > m, the composition of the cone's projection and the Pi-π map equals the π-map at index n composed with the appropriate isomorphism, expressing compatibility at the positive side.

Русский

Для n > m композиция проекции конуса и Pi-π-отображения равна Pi-π-отображению в индексе n, что выражает совместимость на положительной стороне.

LaTeX

$$$\\forall m

Lean4

@[reassoc]
theorem cone_π_app_comp_Pi_π_pos (m n : ℕ) (h : n < m) :
    (cone f).π.app ⟨m⟩ ≫ Pi.π (fun i ↦ if _ : i < m then M i else N i) n =
      Pi.π _ n ≫ eqToHom (functorObj_eq_pos h).symm :=
  by
  simp only [Functor.const_obj_obj, dite_eq_ite, Functor.ofOpSequence_obj, cone_π_app, limMap_π,
    Discrete.functor_obj_eq_as, Discrete.natTrans_app]
  rw [dif_pos h]

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