Theorems · Theorem · category theory
ComplexShape.Embedding.embeddingUpInt_areComplementary
∀ (n₀ n₁ : ℤ), n₀ + 1 = n₁ → (ComplexShape.embeddingUpIntLE n₀).AreComplementary (ComplexShape.embeddingUpIntGE n₁)
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 53 from the axioms · uses propext, Classical.choice, Quot.sound
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.
- ComplexShape.upstatement · cited by 1,123
- ComplexShape.downstatement · cited by 605
- ComplexShape.Embedding.AreComplementarystatement · cited by 32
- ComplexShape.embeddingUpIntLEstatement · cited by 21
- ComplexShape.embeddingUpIntGEstatement · cited by 20
Cited by4
Results whose statement or proof uses this declaration.
- CochainComplex.shortComplexTruncLEX₃ToTruncGEproof · cited by 3
- CochainComplex.g_shortComplexTruncLEX₃ToTruncGEproof · cited by 1
- CochainComplex.acyclic_truncLE_iffproof · cited by 0
- CochainComplex.acyclic_truncGE_iffproof · cited by 0