Theorems · Theorem · algebraic topology
SSet.Subcomplex.Pairing.ofIso_index
∀ {X : SSet} {A : X.Subcomplex} (P : A.Pairing) {Y : SSet} {B : Y.Subcomplex} (e : Y ≅ X) (hA : A.preimage e.hom = B)
(x : ↑P.II) {d : ℕ} (hd : (↑x).dim = d) [inst : P.IsProper], ⋯.index hd = ⋯.index hd- Cited by
- 0 results in Mathlib
- Foundations
- Depth 98 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites35
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- Setstatement · cited by 53,352
- Equivstatement · cited by 8,337
- Oppositestatement · cited by 8,081
- CategoryTheory.Iso.homstatement and proof · cited by 7,684
- CategoryTheory.NatTrans.appproof · cited by 7,406
- Set.Elemstatement and proof · cited by 7,166
- Set.preimageproof · cited by 4,946
- CategoryTheory.ConcreteCategory.homproof · cited by 4,022
- CategoryTheory.Isostatement and proof · cited by 3,963
- SimplexCategorystatement · cited by 2,204
- SSetstatement and proof · cited by 1,283
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.