Theorems · Definition · category theory

ComplexShape.Embedding.AreComplementary.Boundary.indexOfBoundaryGE

{ι : 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₂ → {i₂ : ι₂} → e₂.BoundaryGE i₂ → ι₁

If ac : AreComplementary e₁ e₂ (with e₁ : ComplexShape.Embedding c₁ c and e₂ : ComplexShape.Embedding c₂ c), and i₂ belongs to e₂.BoundaryGE, then this is the (unique) index i₁ of c₁ such that ac.Boundary i₁ i₂.

Defined in: Mathlib.Algebra.Homology.Embedding.AreComplementary
Cited by: 1 results in Mathlib
Foundations: Depth 15 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites5

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

ComplexShapestatement and proof · cited by 1,684
ComplexShape.Embeddingstatement and proof · cited by 337
ComplexShape.Embedding.BoundaryGEstatement and proof · cited by 40
ComplexShape.Embedding.AreComplementarystatement and proof · cited by 32
ComplexShape.Embedding.AreComplementary.Boundary.exists₂proof · cited by 1

Cited by2

Results whose statement or proof uses this declaration.

ComplexShape.Embedding.AreComplementary.Boundary.of_boundaryGEstatement · cited by 0
ComplexShape.Embedding.AreComplementary.Boundary.equivproof · cited by 0