| 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 | 41 mathmath: ComplexShape.embeddingUpIntDownInt_f, AreComplementary.desc'_inl, ComplexShape.embeddingDown'Add_f, prev_f_of_not_boundaryGE, op_f, CochainComplex.homotopyUnop_hom_eq, HomologicalComplex.instQuasiIsoAtฮนTruncLEF, AreComplementary.desc_inr, HomologicalComplex.restriction_X, injective_f, ComplexShape.embeddingUpNat_f, AreComplementary.desc_inl, AreComplementary.exists_iโ, HomologicalComplex.restriction_d, ComplexShape.embeddingUp'Add_f, 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, next_f, next_f_of_not_boundaryLE, AreComplementary.equiv_inr, ComplexShape.embeddingDownIntUpInt_f, ComplexShape.embeddingUpIntGE_f, mk'_f, HomologicalComplex.instQuasiIsoAtฯTruncGEF, rel_iff, 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
|