instIsLEObjSingleFunctor — Mathlib

English

For any X in C and n, the object ((singleFunctor C n).obj X) is LE in degree n.

Русский

Для любого X в C и n объект ((singleFunctor C n).obj X) является LE в степени n.

LaTeX

$$$\forall X \in C,\; \forall n \in \mathbb{Z},\; ((\text{singleFunctor } C n).obj X).IsLE n$$$

Lean4

instance (X : C) (n : ℤ) : ((singleFunctor C n).obj X).IsLE n :=
  by
  let e := (singleFunctorIsoCompQ C n).app X
  dsimp only [Functor.comp_obj] at e
  exact TStructure.t.isLE_of_iso e.symm n

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