| Name | Category | Theorems |
|---|
IsRelIff 📖 | CompData | 12 mathmath: instIsRelIffMk', ComplexShape.instIsRelIffNatIntEmbeddingUpIntLE, instIsRelIffOp, ComplexShape.instIsRelIffNatIntEmbeddingDownNat, ComplexShape.instIsRelIffNatIntEmbeddingUpIntGE, ComplexShape.instIsRelIffIntEmbeddingDownIntUpInt, ComplexShape.instIsRelIffNatIntEmbeddingUpNat, IsTruncLE.toIsRelIff, ComplexShape.instIsRelIffEmbeddingDown'Add, ComplexShape.instIsRelIffEmbeddingUp'Add, ComplexShape.instIsRelIffIntEmbeddingUpIntDownInt, IsTruncGE.toIsRelIff
|
IsTruncGE 📖 | CompData | 4 mathmath: ComplexShape.instIsTruncGENatIntEmbeddingUpIntGE, ComplexShape.instIsTruncGEEmbeddingUp'Add, instIsTruncGEOpOfIsTruncLE, ComplexShape.instIsTruncGENatIntEmbeddingUpNat
|
IsTruncLE 📖 | CompData | 4 mathmath: ComplexShape.instIsTruncLEEmbeddingDown'Add, ComplexShape.instIsTruncLENatIntEmbeddingUpIntLE, instIsTruncLEOpOfIsTruncGE, ComplexShape.instIsTruncLENatIntEmbeddingDownNat
|
f 📖 | CompOp | 51 mathmath: IsTruncGE.mem_next, ComplexShape.embeddingUpIntDownInt_f, mem_prev, AreComplementary.desc'_inl, ComplexShape.embeddingDown'Add_f, prev_f_of_not_boundaryGE, HomologicalComplex.restriction.sc'Iso_inv_τ₃, op_f, CochainComplex.homotopyUnop_hom_eq, HomologicalComplex.instQuasiIsoAtιTruncLEF, HomologicalComplex.restriction.sc'Iso_inv_τ₁, AreComplementary.desc_inr, HomologicalComplex.restriction_X, injective_f, ComplexShape.embeddingUpNat_f, AreComplementary.desc_inl, AreComplementary.exists_i₁, HomologicalComplex.restriction_d, ComplexShape.embeddingUp'Add_f, HomologicalComplex.restriction.sc'Iso_hom_τ₂, IsTruncLE.mem_prev, AreComplementary.exists_i₂, AreComplementary.union, HomologicalComplex.IsSupportedOutside.exactAt, AreComplementary.equiv_inl, prev_f, CochainComplex.homotopyOp_hom_eq, Homotopy.ofExtend_hom, HomologicalComplex.IsStrictlySupportedOutside.isZero, homRestrict.comm_assoc, f_eq_of_r_eq_some, homRestrict.comm, ComplexShape.embeddingUpIntLE_f, HomologicalComplex.extend.instHasHomologyF, ComplexShape.embeddingDownNat_f, HomologicalComplex.restrictionMap_f, HomologicalComplex.restriction.sc'Iso_inv_τ₂, next_f, mem_next, next_f_of_not_boundaryLE, AreComplementary.equiv_inr, ComplexShape.embeddingDownIntUpInt_f, ComplexShape.embeddingUpIntGE_f, mk'_f, HomologicalComplex.restriction.sc'Iso_hom_τ₃, HomologicalComplex.instQuasiIsoAtπTruncGEF, rel_iff, HomologicalComplex.restriction.sc'Iso_hom_τ₁, r_f, rel, AreComplementary.desc'_inr
|
mk' 📖 | CompOp | 2 mathmath: instIsRelIffMk', mk'_f
|
op 📖 | CompOp | 13 mathmath: op_f, HomologicalComplex.extend_op_d_assoc, HomologicalComplex.isStrictlySupportedOutside_op_iff, instIsRelIffOp, instIsTruncLEOpOfIsTruncGE, HomologicalComplex.isSupportedOutside_op_iff, HomologicalComplex.extend_op_d, HomologicalComplex.isStrictlySupported_op_iff, op_boundaryLE_iff, op_boundaryGE_iff, instIsTruncGEOpOfIsTruncLE, HomologicalComplex.isSupported_op_iff, HomologicalComplex.instIsStrictlySupportedOppositeOpOp
|
r 📖 | CompOp | 3 mathmath: r_eq_some, r_eq_none, r_f
|