Structures · Algebra
ComplexShape.Embedding.IsRelIff
An embedding of complex shapes e satisfies e.IsRelIff if the implication
e.rel is an equivalence.
- Defined in
- Mathlib.Algebra.Homology.Embedding.Basic
- Shape
- One type argument · adds rel'
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by2
Concrete types that are instances2
- Int
- Nat
How is a type an instance?
Loading the hierarchy index…
Assumed by118
- HomologicalComplex.restriction
- HomologicalComplex.restrictionXIso
- HomologicalComplex.restrictionMap
- ComplexShape.Embedding.HasLift
- HomologicalComplex.restrictionOpcyclesIso
- HomologicalComplex.restrictionHomologyIso
- HomologicalComplex.stupidTrunc
- ComplexShape.Embedding.homRestrict
- ComplexShape.Embedding.liftExtend
- HomologicalComplex.restriction.sc'Iso
- HomologicalComplex.restrictionCyclesIso
- ComplexShape.Embedding.not_boundaryGE_next
- HomologicalComplex.stupidTruncMap
- ComplexShape.Embedding.restrictionFunctor
- ComplexShape.Embedding.rel_iff
- Homotopy.ofExtend
- ComplexShape.Embedding.homRestrict_f
- HomologicalComplex.stupidTruncXIso
- Homotopy.extend
- ComplexShape.Embedding.homRestrict.f
- HomologicalComplex.restrictionHomologyIso_inv_homologyι_assoc
- ComplexShape.Embedding.not_boundaryGE_next'
- ComplexShape.Embedding.liftExtend.f
- ComplexShape.Embedding.liftExtendfArrowIso
- HomologicalComplex.restrictionHomologyIso_hom_homologyι
- ComplexShape.Embedding.homEquiv
- ComplexShape.Embedding.not_boundaryLE_prev
- HomologicalComplex.pOpcycles_restrictionOpcyclesIso_hom
- ComplexShape.Embedding.homRestrict_comp_extendMap
- ComplexShape.Embedding.liftExtend.f_eq
- HomologicalComplex.pOpcycles_restrictionOpcyclesIso_inv_assoc
- HomologicalComplex.homologyπ_restrictionHomologyIso_hom
- ComplexShape.Embedding.homRestrict.f_eq
- Homotopy.ofExtend_hom
- HomologicalComplex.pOpcycles_restrictionOpcyclesIso_inv
- ComplexShape.Embedding.homRestrict_precomp
- Homotopy.extend_hom_eq
- HomologicalComplex.homotopyEquivalences_extendMap_iff
- ComplexShape.Embedding.liftExtend_f
- ComplexShape.Embedding.stupidTruncFunctor
- ComplexShape.Embedding.homRestrict.comm
- HomologicalComplex.restriction_d
- HomologicalComplex.restriction_d_eq
- HomologicalComplex.stupidTruncMap_stupidTruncXIso_hom
- ComplexShape.Embedding.homRestrict_hasLift
- ComplexShape.Embedding.extendHomotopyFunctor
- ComplexShape.Embedding.homRestrict_liftExtend
- HomologicalComplex.homologyπ_restrictionHomologyIso_inv
- ComplexShape.Embedding.epi_liftExtend_f_iff
- HomologicalComplex.restrictionMap_comp
Ancestors0
No ancestors.