Theorems · Inductive type · category theory

ComplexShape.Embedding.IsTruncLE

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

The condition that the image of the map e.f of an embedding of complex shapes e : Embedding c c' is stable by c'.prev.

Defined in

Mathlib.Algebra.Homology.Embedding.Basic

Cited by

48 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms