Theorems · Inductive type · category theory

ComplexShape.Embedding.IsRelIff

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

An embedding of complex shapes e satisfies e.IsRelIff if the implication e.rel is an equivalence.

Defined in

Mathlib.Algebra.Homology.Embedding.Basic

Cited by

88 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms