Mathlib Map

Theorems · Theorem · category theory

HomotopicalAlgebra.RightHomotopyRel.trans

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} [inst_1 : HomotopicalAlgebra.ModelCategory C]
  {f₀ f₁ f₂ : X ⟶ Y} [HomotopicalAlgebra.IsFibrant Y],
  HomotopicalAlgebra.RightHomotopyRel f₀ f₁ →
    HomotopicalAlgebra.RightHomotopyRel f₁ f₂ → HomotopicalAlgebra.RightHomotopyRel f₀ f₂
Defined in
Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
Cited by
1 results in Mathlib
Foundations
Depth 75 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
CategoryTheory.CategoryHomotopicalAlgebra.ModelCategoryHomotopicalAlgebra.IsFibrant
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

HomotopicalAlgebra.RightHomotopyRel.equivalence · cited by 2RightHomotopyRel.equivale…CategoryTheory.Category · cited by 32673CategoryTheory.CategoryQuiver.Hom · cited by 32603Quiver.HomHomotopicalAlgebra.ModelCategory · cited by 141HomotopicalAlgebra.ModelC…HomotopicalAlgebra.IsFibrant · cited by 56HomotopicalAlgebra.IsFibr…HomotopicalAlgebra.PathObject · cited by 32HomotopicalAlgebra.PathOb…HomotopicalAlgebra.RightHomotopyRel · cited by 22HomotopicalAlgebra.RightH…HomotopicalAlgebra.PathObject.RightHomotopy · cited by 14PathObject.RightHomotopyHomotopicalAlgebra.PathObject.IsGood · cited by 11PathObject.IsGoodHomotopicalAlgebra.PathObject.RightHomotopy.rightHomotopyRel · cited by 3RightHomotopy.rightHomoto…HomotopicalAlgebra.RightHomotopyRel.exists_good_pathObject · cited by 3RightHomotopyRel.exists_g…HomotopicalAlgebra.PathObject.RightHomotopy.trans · cited by 1RightHomotopy.transRightHomotopyRel.transCITED BYCITES

Cites11

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by1

Results whose statement or proof uses this declaration.