Loogle!

Result

Found 88 declarations mentioning CategoryTheory.Triangulated.TStructure.truncGE.

CategoryTheory.Triangulated.TStructure.truncGE 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) : CategoryTheory.Functor C C
CategoryTheory.Triangulated.TStructure.instAdditiveTruncGE 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) : (t.truncGE n).Additive
CategoryTheory.Triangulated.TStructure.instIsGEObjTruncGE 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (X : C) (n : ℤ) : t.IsGE ((t.truncGE n).obj X) n
CategoryTheory.Triangulated.TStructure.isGE_truncGE_obj 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (X : C) (a b : ℤ) (hn : b ≤ a := by lia) : t.IsGE ((t.truncGE a).obj X) b
CategoryTheory.Triangulated.TStructure.truncGEπ 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) : CategoryTheory.Functor.id C ⟶ t.truncGE n
CategoryTheory.Triangulated.TStructure.instIsGEObjTruncGE_1 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (X : C) (a b : ℤ) [t.IsGE X a] : t.IsGE ((t.truncGE b).obj X) a
CategoryTheory.Triangulated.TStructure.triangleLTGE_obj_obj₃ 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) (j : C) : ((t.triangleLTGE n).obj j).obj₃ = (t.truncGE n).obj j
CategoryTheory.Triangulated.TStructure.descTruncGE 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) {X Y : C} (f : X ⟶ Y) (n : ℤ) [t.IsGE Y n] : (t.truncGE n).obj X ⟶ Y
CategoryTheory.Triangulated.TStructure.instIsLEObjTruncGE 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) [CategoryTheory.IsTriangulated C] (X : C) (a b : ℤ) [t.IsLE X b] : t.IsLE ((t.truncGE a).obj X) b
CategoryTheory.Triangulated.TStructure.isZero_truncGE_obj_of_isLE 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) (X : C) [t.IsLE X n₀] : CategoryTheory.Limits.IsZero ((t.truncGE n₁).obj X)
CategoryTheory.Triangulated.TStructure.isLE_iff_isZero_truncGE_obj 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) (X : C) : t.IsLE X n₀ ↔ CategoryTheory.Limits.IsZero ((t.truncGE n₁).obj X)
CategoryTheory.Triangulated.TStructure.natTransTruncGEOfLE 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a ≤ b) : t.truncGE a ⟶ t.truncGE b
CategoryTheory.Triangulated.TStructure.truncGEδLT 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) : t.truncGE n ⟶ (t.truncLT n).comp (CategoryTheory.shiftFunctor C 1)
CategoryTheory.Triangulated.TStructure.triangleLTLTGELT_obj_obj₃ 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a ≤ b) (j : C) : ((t.triangleLTLTGELT a b h).obj j).obj₃ = (t.truncGE a).obj ((t.truncLT b).obj j)
CategoryTheory.Triangulated.TStructure.instIsIsoAppTruncGEπOfIsGE 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (X : C) (n : ℤ) [t.IsGE X n] : CategoryTheory.IsIso ((t.truncGEπ n).app X)
CategoryTheory.Triangulated.TStructure.isGE_iff_isIso_truncGEπ_app 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) (X : C) : t.IsGE X n ↔ CategoryTheory.IsIso ((t.truncGEπ n).app X)
CategoryTheory.Triangulated.TStructure.natTransTruncGEOfLE_refl 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (a : ℤ) : t.natTransTruncGEOfLE a a ⋯ = CategoryTheory.CategoryStruct.id (t.truncGE a)
CategoryTheory.Triangulated.TStructure.triangleLTGE_obj_mor₂ 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) (j : C) : ((t.triangleLTGE n).obj j).mor₂ = (t.truncGEπ n).app j
CategoryTheory.Triangulated.TStructure.natTransTruncGEOfLE_refl_app 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (a : ℤ) (X : C) : (t.natTransTruncGEOfLE a a ⋯).app X = CategoryTheory.CategoryStruct.id ((t.truncGE a).obj X)
CategoryTheory.Triangulated.TStructure.π_descTruncGE 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) {X Y : C} (f : X ⟶ Y) (n : ℤ) [t.IsGE Y n] : CategoryTheory.CategoryStruct.comp ((t.truncGEπ n).app X) (t.descTruncGE f n) = f
CategoryTheory.Triangulated.TStructure.π_natTransTruncGEOfLE 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a ≤ b) : CategoryTheory.CategoryStruct.comp (t.truncGEπ a) (t.natTransTruncGEOfLE a b h) = t.truncGEπ b
CategoryTheory.Triangulated.TStructure.instIsIsoMapTruncGEAppTruncGEπ 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) [CategoryTheory.IsTriangulated C] (X : C) (n : ℤ) : CategoryTheory.IsIso ((t.truncGE n).map ((t.truncGEπ n).app X))
CategoryTheory.Triangulated.TStructure.triangleLTLTGELT_obj_mor₂ 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a ≤ b) (j : C) : ((t.triangleLTLTGELT a b h).obj j).mor₂ = (t.truncGEπ a).app ((t.truncLT b).obj j)
CategoryTheory.Triangulated.TStructure.triangleLTGE_obj_mor₃ 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) (j : C) : ((t.triangleLTGE n).obj j).mor₃ = (t.truncGEδLT n).app j
CategoryTheory.Triangulated.TStructure.isIso₂_truncGE_map_of_isLE 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) [CategoryTheory.IsTriangulated C] (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) (h₁ : t.IsLE T.obj₁ n₀) : CategoryTheory.IsIso ((t.truncGE n₁).map T.mor₂)
CategoryTheory.Triangulated.TStructure.isIso_truncGE_map_truncGEπ_app 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) [CategoryTheory.IsTriangulated C] (a b : ℤ) (h : b ≤ a) (X : C) : CategoryTheory.IsIso ((t.truncGE a).map ((t.truncGEπ b).app X))
CategoryTheory.Triangulated.TStructure.π_descTruncGE_assoc 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) {X Y : C} (f : X ⟶ Y) (n : ℤ) [t.IsGE Y n] {Z : C} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp ((t.truncGEπ n).app X) (CategoryTheory.CategoryStruct.comp (t.descTruncGE f n) h) = CategoryTheory.CategoryStruct.comp f h
CategoryTheory.Triangulated.TStructure.descTruncGE_aux 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) {X Y : C} (f : X ⟶ Y) (n : ℤ) [t.IsGE Y n] : ∃ f', f = CategoryTheory.CategoryStruct.comp ((t.truncGEπ n).app X) f'
CategoryTheory.Triangulated.TStructure.natTransTruncGEOfLE_trans 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (a b c : ℤ) (hab : a ≤ b) (hbc : b ≤ c) : CategoryTheory.CategoryStruct.comp (t.natTransTruncGEOfLE a b hab) (t.natTransTruncGEOfLE b c hbc) = t.natTransTruncGEOfLE a c ⋯
CategoryTheory.Triangulated.TStructure.instIsIsoAppTruncLTιObjTruncGETruncLT 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) [CategoryTheory.IsTriangulated C] (a b : ℤ) (X : C) : CategoryTheory.IsIso ((t.truncLTι b).app ((t.truncGE a).obj ((t.truncLT b).obj X)))
CategoryTheory.Triangulated.TStructure.truncGE_map_truncGEπ_app 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) (X : C) : (t.truncGE n).map ((t.truncGEπ n).app X) = (t.truncGEπ n).app ((t.truncGE n).obj X)
CategoryTheory.Triangulated.TStructure.π_natTransTruncGEOfLE_app 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a ≤ b) (X : C) : CategoryTheory.CategoryStruct.comp ((t.truncGEπ a).app X) ((t.natTransTruncGEOfLE a b h).app X) = (t.truncGEπ b).app X
CategoryTheory.Triangulated.TStructure.truncGEπ_naturality 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) {X Y : C} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp ((t.truncGEπ n).app X) ((t.truncGE n).map f) = CategoryTheory.CategoryStruct.comp f ((t.truncGEπ n).app Y)
CategoryTheory.Triangulated.TStructure.π_natTransTruncGEOfLE_assoc 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a ≤ b) {Z : CategoryTheory.Functor C C} (h✝ : t.truncGE b ⟶ Z) : CategoryTheory.CategoryStruct.comp (t.truncGEπ a) (CategoryTheory.CategoryStruct.comp (t.natTransTruncGEOfLE a b h) h✝) = CategoryTheory.CategoryStruct.comp (t.truncGEπ b) h✝
CategoryTheory.Triangulated.TStructure.truncGEπ_naturality_assoc 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) {X Y : C} (f : X ⟶ Y) {Z : C} (h : (t.truncGE n).obj Y ⟶ Z) : CategoryTheory.CategoryStruct.comp ((t.truncGEπ n).app X) (CategoryTheory.CategoryStruct.comp ((t.truncGE n).map f) h) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp ((t.truncGEπ n).app Y) h)
CategoryTheory.Triangulated.TStructure.truncLTι_comp_truncGEπ 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) : CategoryTheory.CategoryStruct.comp (t.truncLTι n) (t.truncGEπ n) = 0
CategoryTheory.Triangulated.TStructure.π_natTransTruncGEOfLE_app_assoc 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a ≤ b) (X : C) {Z : C} (h✝ : (t.truncGE b).obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((t.truncGEπ a).app X) (CategoryTheory.CategoryStruct.comp ((t.natTransTruncGEOfLE a b h).app X) h✝) = CategoryTheory.CategoryStruct.comp ((t.truncGEπ b).app X) h✝
CategoryTheory.Triangulated.TStructure.natTransTruncGEOfLE_trans_app 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (a b c : ℤ) (hab : a ≤ b) (hbc : b ≤ c) (X : C) : CategoryTheory.CategoryStruct.comp ((t.natTransTruncGEOfLE a b hab).app X) ((t.natTransTruncGEOfLE b c hbc).app X) = (t.natTransTruncGEOfLE a c ⋯).app X
CategoryTheory.Triangulated.TStructure.from_truncGE_obj_ext 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) {n : ℤ} {X Y : C} {f₁ f₂ : (t.truncGE n).obj X ⟶ Y} (h : CategoryTheory.CategoryStruct.comp ((t.truncGEπ n).app X) f₁ = CategoryTheory.CategoryStruct.comp ((t.truncGEπ n).app X) f₂) [t.IsGE Y n] : f₁ = f₂
CategoryTheory.Triangulated.TStructure.instIsIsoMapTruncLTTruncGEAppTruncLTι 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) [CategoryTheory.IsTriangulated C] (a b : ℤ) (X : C) : CategoryTheory.IsIso ((t.truncLT b).map ((t.truncGE a).map ((t.truncLTι b).app X)))
CategoryTheory.Triangulated.TStructure.truncLTι_comp_truncGEπ_app 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) (X : C) : CategoryTheory.CategoryStruct.comp ((t.truncLTι n).app X) ((t.truncGEπ n).app X) = 0
CategoryTheory.Triangulated.TStructure.truncGE_map_truncGEπ_app_assoc 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) (X : C) {Z : C} (h : (t.truncGE n).obj ((t.truncGE n).obj X) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((t.truncGE n).map ((t.truncGEπ n).app X)) h = CategoryTheory.CategoryStruct.comp ((t.truncGEπ n).app ((t.truncGE n).obj X)) h
CategoryTheory.Triangulated.TStructure.truncGEπ_comp_truncGEδLT 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) : CategoryTheory.CategoryStruct.comp (t.truncGEπ n) (t.truncGEδLT n) = 0
CategoryTheory.Triangulated.TStructure.truncGEδLT_comp_whiskerRight_natTransTruncLTOfLE 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a ≤ b) : CategoryTheory.CategoryStruct.comp (t.truncGEδLT a) (CategoryTheory.Functor.whiskerRight (t.natTransTruncLTOfLE a b h) (CategoryTheory.shiftFunctor C 1)) = CategoryTheory.CategoryStruct.comp (t.natTransTruncGEOfLE a b h) (t.truncGEδLT b)
CategoryTheory.Triangulated.TStructure.truncLTι_comp_truncGEπ_assoc 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) {Z : CategoryTheory.Functor C C} (h : t.truncGE n ⟶ Z) : CategoryTheory.CategoryStruct.comp (t.truncLTι n) (CategoryTheory.CategoryStruct.comp (t.truncGEπ n) h) = CategoryTheory.CategoryStruct.comp 0 h
CategoryTheory.Triangulated.TStructure.truncLTι_comp_truncGEπ_app_assoc 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) (X : C) {Z : C} (h : (t.truncGE n).obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((t.truncLTι n).app X) (CategoryTheory.CategoryStruct.comp ((t.truncGEπ n).app X) h) = CategoryTheory.CategoryStruct.comp 0 h
CategoryTheory.Triangulated.TStructure.truncGEδLT_comp_truncLTι 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) : CategoryTheory.CategoryStruct.comp (t.truncGEδLT n) (CategoryTheory.Functor.whiskerRight (t.truncLTι n) (CategoryTheory.shiftFunctor C 1)) = 0
CategoryTheory.Triangulated.TStructure.truncGEπ_comp_truncGEδLT_app 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) (X : C) : CategoryTheory.CategoryStruct.comp ((t.truncGEπ n).app X) ((t.truncGEδLT n).app X) = 0
CategoryTheory.Triangulated.TStructure.triangleLTGE_map_hom₂ 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) {X✝ Y✝ : C} (φ : X✝ ⟶ Y✝) : ((t.triangleLTGE n).map φ).hom₂ = φ
CategoryTheory.Triangulated.TStructure.truncGEπ_comp_truncGEδLT_assoc 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) {Z : CategoryTheory.Functor C C} (h : (t.truncLT n).comp (CategoryTheory.shiftFunctor C 1) ⟶ Z) : CategoryTheory.CategoryStruct.comp (t.truncGEπ n) (CategoryTheory.CategoryStruct.comp (t.truncGEδLT n) h) = CategoryTheory.CategoryStruct.comp 0 h
CategoryTheory.Triangulated.TStructure.isIso_truncGE_map_iff 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) {Y Z : C} (g : Y ⟶ Z) (n₀ n₁ : ℤ) (hn : n₀ + 1 = n₁) : CategoryTheory.IsIso ((t.truncGE n₁).map g) ↔ ∃ X f h, ∃ (_ : CategoryTheory.Pretriangulated.Triangle.mk f (CategoryTheory.CategoryStruct.comp g ((t.truncGEπ n₁).app Z)) h ∈ CategoryTheory.Pretriangulated.distinguishedTriangles), t.IsLE X n₀
CategoryTheory.Triangulated.TStructure.truncGEδLT_comp_truncLTι_app 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) (X : C) : CategoryTheory.CategoryStruct.comp ((t.truncGEδLT n).app X) ((CategoryTheory.shiftFunctor C 1).map ((t.truncLTι n).app X)) = 0
CategoryTheory.Triangulated.TStructure.truncGEδLT_comp_whiskerRight_natTransTruncLTOfLE_assoc 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a ≤ b) {Z : CategoryTheory.Functor C C} (h✝ : (t.truncLT b).comp (CategoryTheory.shiftFunctor C 1) ⟶ Z) : CategoryTheory.CategoryStruct.comp (t.truncGEδLT a) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (t.natTransTruncLTOfLE a b h) (CategoryTheory.shiftFunctor C 1)) h✝) = CategoryTheory.CategoryStruct.comp (t.natTransTruncGEOfLE a b h) (CategoryTheory.CategoryStruct.comp (t.truncGEδLT b) h✝)
CategoryTheory.Triangulated.TStructure.truncGEπ_comp_truncGEδLT_app_assoc 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) (X : C) {Z : C} (h : (CategoryTheory.shiftFunctor C 1).obj ((t.truncLT n).obj X) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((t.truncGEπ n).app X) (CategoryTheory.CategoryStruct.comp ((t.truncGEδLT n).app X) h) = CategoryTheory.CategoryStruct.comp 0 h
CategoryTheory.Triangulated.TStructure.triangleLTGE_map_hom₁ 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) {X✝ Y✝ : C} (φ : X✝ ⟶ Y✝) : ((t.triangleLTGE n).map φ).hom₁ = (t.truncLT n).map φ
CategoryTheory.Triangulated.TStructure.triangleLTGE_map_hom₃ 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) {X✝ Y✝ : C} (φ : X✝ ⟶ Y✝) : ((t.triangleLTGE n).map φ).hom₃ = (t.truncGE n).map φ
CategoryTheory.Triangulated.TStructure.triangleLTLTGELT_obj_mor₃ 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a ≤ b) (j : C) : ((t.triangleLTLTGELT a b h).obj j).mor₃ = CategoryTheory.CategoryStruct.comp ((t.truncGEδLT a).app ((t.truncLT b).obj j)) ((CategoryTheory.shiftFunctor C 1).map ((t.truncLT a).map ((t.truncLTι b).app j)))
CategoryTheory.Triangulated.TStructure.truncGELTδLT_app 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (X : C) : (t.truncGELTδLT a b).app X = CategoryTheory.CategoryStruct.comp ((t.truncGEδLT a).app ((t.truncLT b).obj X)) ((CategoryTheory.shiftFunctor C 1).map ((t.truncLT a).map ((t.truncLTι b).app X)))
CategoryTheory.Triangulated.TStructure.truncLT_map_truncGE_map_truncLTι_app_fac 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) [CategoryTheory.IsTriangulated C] (a b : ℤ) (X : C) : CategoryTheory.CategoryStruct.comp ((t.truncLTι b).app ((t.truncGE a).obj ((t.truncLT b).obj X))) ((t.truncGELTToLTGE a b).app X) = (t.truncLT b).map ((t.truncGE a).map ((t.truncLTι b).app X))
CategoryTheory.Triangulated.TStructure.truncGEδLT_comp_natTransTruncLTOfLE_app 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a ≤ b) (X : C) : CategoryTheory.CategoryStruct.comp ((t.truncGEδLT a).app X) ((CategoryTheory.shiftFunctor C 1).map ((t.natTransTruncLTOfLE a b h).app X)) = CategoryTheory.CategoryStruct.comp ((t.natTransTruncGEOfLE a b h).app X) ((t.truncGEδLT b).app X)
CategoryTheory.Triangulated.TStructure.truncGEδLT_comp_truncLTι_assoc 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) {Z : CategoryTheory.Functor C C} (h : (CategoryTheory.Functor.id C).comp (CategoryTheory.shiftFunctor C 1) ⟶ Z) : CategoryTheory.CategoryStruct.comp (t.truncGEδLT n) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (t.truncLTι n) (CategoryTheory.shiftFunctor C 1)) h) = CategoryTheory.CategoryStruct.comp 0 h
CategoryTheory.Triangulated.TStructure.truncGELTToLTGE_app_pentagon 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) [CategoryTheory.IsTriangulated C] (a b : ℤ) (X : C) : CategoryTheory.CategoryStruct.comp ((t.truncGEπ a).app ((t.truncLT b).obj X)) (CategoryTheory.CategoryStruct.comp ((t.truncGELTToLTGE a b).app X) ((t.truncLTι b).app ((t.truncGE a).obj X))) = CategoryTheory.CategoryStruct.comp ((t.truncLTι b).app X) ((t.truncGEπ a).app X)
CategoryTheory.Triangulated.TStructure.truncGEδLT_comp_truncLTι_app_assoc 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) (X : C) {Z : C} (h : (CategoryTheory.shiftFunctor C 1).obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((t.truncGEδLT n).app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C 1).map ((t.truncLTι n).app X)) h) = CategoryTheory.CategoryStruct.comp 0 h
CategoryTheory.Triangulated.TStructure.truncGELTToLTGE_app_pentagon_assoc 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) [CategoryTheory.IsTriangulated C] (a b : ℤ) (X : C) {Z : C} (h : (t.truncGE a).obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((t.truncGEπ a).app ((t.truncLT b).obj X)) (CategoryTheory.CategoryStruct.comp ((t.truncGELTToLTGE a b).app X) (CategoryTheory.CategoryStruct.comp ((t.truncLTι b).app ((t.truncGE a).obj X)) h)) = CategoryTheory.CategoryStruct.comp ((t.truncLTι b).app X) (CategoryTheory.CategoryStruct.comp ((t.truncGEπ a).app X) h)
CategoryTheory.Triangulated.TStructure.truncGEδLT_comp_natTransTruncLTOfLE_app_assoc 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a ≤ b) (X : C) {Z : C} (h✝ : (CategoryTheory.shiftFunctor C 1).obj ((t.truncLT b).obj X) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((t.truncGEδLT a).app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C 1).map ((t.natTransTruncLTOfLE a b h).app X)) h✝) = CategoryTheory.CategoryStruct.comp ((t.natTransTruncGEOfLE a b h).app X) (CategoryTheory.CategoryStruct.comp ((t.truncGEδLT b).app X) h✝)
CategoryTheory.Triangulated.TStructure.truncGELTToLTGE_app_pentagon_uniqueness 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) [CategoryTheory.IsTriangulated C] {a b : ℤ} {X : C} (φ : (t.truncGELT a b).obj X ⟶ (t.truncLTGE a b).obj X) (hφ : CategoryTheory.CategoryStruct.comp ((t.truncGEπ a).app ((t.truncLT b).obj X)) (CategoryTheory.CategoryStruct.comp φ ((t.truncLTι b).app ((t.truncGE a).obj X))) = CategoryTheory.CategoryStruct.comp ((t.truncLTι b).app X) ((t.truncGEπ a).app X)) : (t.truncGELTToLTGE a b).app X = φ
CategoryTheory.Triangulated.TStructure.truncLT_map_truncGE_map_truncLTι_app_fac_assoc 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) [CategoryTheory.IsTriangulated C] (a b : ℤ) (X : C) {Z : C} (h : (t.truncLT b).obj ((t.truncGE a).obj X) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((t.truncLTι b).app ((t.truncGE a).obj ((t.truncLT b).obj X))) (CategoryTheory.CategoryStruct.comp ((t.truncGELTToLTGE a b).app X) h) = CategoryTheory.CategoryStruct.comp ((t.truncLT b).map ((t.truncGE a).map ((t.truncLTι b).app X))) h
CategoryTheory.Triangulated.TStructure.triangleLTLTGELT_map_hom₁ 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a ≤ b) {X✝ Y✝ : C} (φ : X✝ ⟶ Y✝) : ((t.triangleLTLTGELT a b h).map φ).hom₁ = (t.truncLT a).map φ
CategoryTheory.Triangulated.TStructure.triangleLTLTGELT_map_hom₂ 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a ≤ b) {X✝ Y✝ : C} (φ : X✝ ⟶ Y✝) : ((t.triangleLTLTGELT a b h).map φ).hom₂ = (t.truncLT b).map φ
CategoryTheory.Triangulated.TStructure.triangleLTLTGELT_map_hom₃ 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a ≤ b) {X✝ Y✝ : C} (φ : X✝ ⟶ Y✝) : ((t.triangleLTLTGELT a b h).map φ).hom₃ = (t.truncGE a).map ((t.truncLT b).map φ)
CategoryTheory.Triangulated.TStructure.truncGTIsoTruncGE 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a + 1 = b) : t.truncGT a ≅ t.truncGE b
CategoryTheory.Triangulated.TStructure.triangleLEGE_obj_obj₃ 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a + 1 = b) (j : C) : ((t.triangleLEGE a b h).obj j).obj₃ = (t.truncGE b).obj j
CategoryTheory.Triangulated.TStructure.truncGEδLE 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a + 1 = b) : t.truncGE b ⟶ (t.truncLE a).comp (CategoryTheory.shiftFunctor C 1)
CategoryTheory.Triangulated.TStructure.triangleLEGE_obj_mor₂ 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a + 1 = b) (j : C) : ((t.triangleLEGE a b h).obj j).mor₂ = (t.truncGEπ b).app j
CategoryTheory.Triangulated.TStructure.π_truncGTIsoTruncGE_hom 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a + 1 = b) : CategoryTheory.CategoryStruct.comp (t.truncGTπ a) (t.truncGTIsoTruncGE a b h).hom = t.truncGEπ b
CategoryTheory.Triangulated.TStructure.π_truncGTIsoTruncGE_inv 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a + 1 = b) : CategoryTheory.CategoryStruct.comp (t.truncGEπ b) (t.truncGTIsoTruncGE a b h).inv = t.truncGTπ a
CategoryTheory.Triangulated.TStructure.triangleLEGE_obj_mor₃ 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a + 1 = b) (j : C) : ((t.triangleLEGE a b h).obj j).mor₃ = (t.truncGEδLE a b h).app j
CategoryTheory.Triangulated.TStructure.π_truncGTIsoTruncGE_hom_ι_app 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a + 1 = b) (X : C) : CategoryTheory.CategoryStruct.comp ((t.truncGTπ a).app X) ((t.truncGTIsoTruncGE a b h).hom.app X) = (t.truncGEπ b).app X
CategoryTheory.Triangulated.TStructure.π_truncGTIsoTruncGE_inv_ι_app 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a + 1 = b) (X : C) : CategoryTheory.CategoryStruct.comp ((t.truncGEπ b).app X) ((t.truncGTIsoTruncGE a b h).inv.app X) = (t.truncGTπ a).app X
CategoryTheory.Triangulated.TStructure.π_truncGTIsoTruncGE_hom_assoc 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a + 1 = b) {Z : CategoryTheory.Functor C C} (h✝ : t.truncGE b ⟶ Z) : CategoryTheory.CategoryStruct.comp (t.truncGTπ a) (CategoryTheory.CategoryStruct.comp (t.truncGTIsoTruncGE a b h).hom h✝) = CategoryTheory.CategoryStruct.comp (t.truncGEπ b) h✝
CategoryTheory.Triangulated.TStructure.π_truncGTIsoTruncGE_inv_assoc 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a + 1 = b) {Z : CategoryTheory.Functor C C} (h✝ : t.truncGT a ⟶ Z) : CategoryTheory.CategoryStruct.comp (t.truncGEπ b) (CategoryTheory.CategoryStruct.comp (t.truncGTIsoTruncGE a b h).inv h✝) = CategoryTheory.CategoryStruct.comp (t.truncGTπ a) h✝
CategoryTheory.Triangulated.TStructure.π_truncGTIsoTruncGE_hom_ι_app_assoc 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a + 1 = b) (X : C) {Z : C} (h✝ : (t.truncGE b).obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((t.truncGTπ a).app X) (CategoryTheory.CategoryStruct.comp ((t.truncGTIsoTruncGE a b h).hom.app X) h✝) = CategoryTheory.CategoryStruct.comp ((t.truncGEπ b).app X) h✝
CategoryTheory.Triangulated.TStructure.π_truncGTIsoTruncGE_inv_ι_app_assoc 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a + 1 = b) (X : C) {Z : C} (h✝ : (t.truncGT a).obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((t.truncGEπ b).app X) (CategoryTheory.CategoryStruct.comp ((t.truncGTIsoTruncGE a b h).inv.app X) h✝) = CategoryTheory.CategoryStruct.comp ((t.truncGTπ a).app X) h✝
CategoryTheory.Triangulated.TStructure.triangleLEGE_map_hom₂ 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a + 1 = b) {X✝ Y✝ : C} (φ : X✝ ⟶ Y✝) : ((t.triangleLEGE a b h).map φ).hom₂ = φ
CategoryTheory.Triangulated.TStructure.triangleLEGE_map_hom₁ 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a + 1 = b) {X✝ Y✝ : C} (φ : X✝ ⟶ Y✝) : ((t.triangleLEGE a b h).map φ).hom₁ = (t.truncLE a).map φ
CategoryTheory.Triangulated.TStructure.triangleLEGE_map_hom₃ 📋 Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a + 1 = b) {X✝ Y✝ : C} (φ : X✝ ⟶ Y✝) : ((t.triangleLEGE a b h).map φ).hom₃ = (t.truncGE b).map φ
CategoryTheory.ObjectProperty.HasInducedTStructure.mk' 📋 Mathlib.CategoryTheory.Triangulated.TStructure.Induced
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] {P : CategoryTheory.ObjectProperty C} [P.IsTriangulated] {t : CategoryTheory.Triangulated.TStructure C} (h : ∀ (X : C), P X → ∀ (n : ℤ), P ((t.truncLE n).obj X) ∧ P ((t.truncGE n).obj X)) : P.HasInducedTStructure t
CategoryTheory.Triangulated.TStructure.eTruncGE_obj_coe 📋 Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) : t.eTruncGE.obj (WithBotTop.coe n) = t.truncGE n

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

By constant:
🔍 Real.sin
finds all lemmas whose statement somehow mentions the sine function.
By lemma name substring:
🔍 "differ"
finds all lemmas that have "differ" somewhere in their lemma name.
By subexpression:
🔍 _ * (_ ^ _)
finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

The pattern can also be non-linear, as in
🔍 Real.sqrt ?a * Real.sqrt ?a

If the pattern has parameters, they are matched in any order. Both of these will find List.map:
🔍 (?a -> ?b) -> List ?a -> List ?b
🔍 List ?a -> (?a -> ?b) -> List ?b
By main conclusion:
🔍 |- tsum _ = _ * tsum _
finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
🔍 |- _ < _ → tsum _ < tsum _
will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.
You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision 69fae59