Theorems · Inductive type · category theory

ComplexShape.Embedding.IsTruncGE

{ι : 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'.next.

Defined in

Mathlib.Algebra.Homology.Embedding.Basic

Cited by

56 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms