Theorems · Theorem · category theory

HomotopicalAlgebra.RelativeCellComplex.Cells.mk.inj

∀ {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

1 results in Mathlib

Foundations

Depth 26 from the axioms · uses propext