Theorems · Definition · category theory

ComplexShape.Embedding.op

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

The opposite embedding in Embedding c.symm c'.symm of e : Embedding c c'.

Defined in

Mathlib.Algebra.Homology.Embedding.Basic

Cited by

26 results in Mathlib

Foundations

Depth 4 from the axioms · uses no axioms