Theorems · Theorem · category theory

HomotopicalAlgebra.RelativeCellComplex.Cells.mk.injEq

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w'} [inst_1 : LinearOrder J] [inst_2 : OrderBot J]
  [inst_3 : SuccOrder J] [inst_4 : WellFoundedLT J] {α : J → Type t} {A B : (j : J) → α j → C}
  {basicCell : (j : J) → (i : α j) → A j i ⟶ B j i} {X Y : C} {f : X ⟶ Y}
  {c : HomotopicalAlgebra.RelativeCellComplex basicCell f} (j : J) (hj : ¬IsMax j) (k : (c.attachCells j hj).ι)
  (j_1 : J) (hj_1 : ¬IsMax j_1) (k_1 : (c.attachCells j_1 hj_1).ι),
  ({ j := j, hj := hj, k := k } = { j := j_1, hj := hj_1, k := k_1 }) = (j = j_1 ∧ k ≍ k_1)

Defined in

Mathlib.AlgebraicTopology.RelativeCellComplex.Basic

Cited by

0 results in Mathlib

Foundations

Depth 27 from the axioms · uses propext

Assumes

CategoryTheory.CategoryLinearOrderOrderBotSuccOrderWellFoundedLT