IsInvertedBy₃ — Mathlib

English

Corresponding equivalence in the reverse direction comparing distTriang in D with the image under L.

Русский

Эквивалентность в обратном направлении между distTriang в D и образом через L.

LaTeX

$$$T\in L.essImageDistTriang \iff T\in distTriang(D)$$$

Lean4

/-- Classes of morphisms `W₁ : MorphismProperty C₁`, `W₂ : MorphismProperty C₂` and
`W₃ : MorphismProperty C₃` are said to be inverted by `F : C₁ ⥤ C₂ ⥤ C₃ ⥤ E` if
`W₁.prod (W₂.prod W₃)` is inverted by the
functor `currying₃.functor.obj F : C₁ × C₂ × C₃ ⥤ E`. -/
def IsInvertedBy₃ (W₁ : MorphismProperty C₁) (W₂ : MorphismProperty C₂) (W₃ : MorphismProperty C₃)
    (F : C₁ ⥤ C₂ ⥤ C₃ ⥤ E) : Prop :=
  (W₁.prod (W₂.prod W₃)).IsInvertedBy (currying₃.functor.obj F)

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