Theorems · Definition · category theory

ComplexShape.Embedding.AreComplementary.Boundary.equiv

{ι : Type u_1} →
  {ι₁ : Type u_2} →
    {ι₂ : Type u_3} →
      {c : ComplexShape ι} →
        {c₁ : ComplexShape ι₁} →
          {c₂ : ComplexShape ι₂} →
            {e₁ : c₁.Embedding c} →
              {e₂ : c₂.Embedding c} → e₁.AreComplementary e₂ → Subtype e₁.BoundaryLE ≃ Subtype e₂.BoundaryGE

The bijection Subtype e₁.BoundaryLE ≃ Subtype e₂.BoundaryGE when e₁ and e₂ are complementary embeddings of complex shapes.

Defined in

Mathlib.Algebra.Homology.Embedding.AreComplementary

Cited by

0 results in Mathlib

Foundations

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