Theorems · Definition · category theory

ComplexShape.Embedding.f

{ι : Type u_1} → {ι' : Type u_2} → {c : ComplexShape ι} → {c' : ComplexShape ι'} → c.Embedding c' → ι → ι'

the map between the underlying types of indices

Defined in

Mathlib.Algebra.Homology.Embedding.Basic

Cited by

251 results in Mathlib

Foundations

Depth 2 from the axioms, rests on 3 definitions · uses no axioms