Theorems · Definition · category theory

ComplexShape.Embedding.BoundaryGE

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

The lower boundary of an embedding e : Embedding c c', as a predicate on ι. It is satisfied by j : ι when there exists i' : ι' not in the image of e.f such that c'.Rel i' (e.f j).

Defined in

Mathlib.Algebra.Homology.Embedding.Boundary

Cited by

40 results in Mathlib

Foundations

Depth 13 from the axioms · uses propext, Classical.choice, Quot.sound