Structures · Algebra
ComplexShape.Embedding.IsTruncLE
The condition that the image of the map e.f of an embedding of
complex shapes e : Embedding c c' is stable by c'.prev.
- Defined in
- Mathlib.Algebra.Homology.Embedding.Basic
- Shape
- One type argument · adds mem_prev
Extends1
Extended by0
Nothing extends this class yet.
Concrete types that are instances1
- Nat
How is a type an instance?
Loading the hierarchy index…
Assumed by81
- HomologicalComplex.truncLE
- HomologicalComplex.truncLE'
- HomologicalComplex.shortComplexTruncLE
- HomologicalComplex.ιTruncLE
- HomologicalComplex.truncLE'Map
- HomologicalComplex.truncLEMap
- HomologicalComplex.truncLE'ToRestriction
- HomologicalComplex.shortComplexTruncLE_shortExact
- ComplexShape.Embedding.truncLEFunctor
- HomologicalComplex.truncLE'XIso
- ComplexShape.Embedding.truncLE'Functor
- HomologicalComplex.shortComplexTruncLEX₃ToTruncGE
- HomologicalComplex.acyclic_truncLE_iff_isSupportedOutside
- HomologicalComplex.ιTruncLE_naturality
- HomologicalComplex.g_shortComplexTruncLEX₃ToTruncGE
- HomologicalComplex.truncLE'XIsoCycles
- HomologicalComplex.quasiIso_ιTruncLE_iff_isSupported
- ComplexShape.Embedding.truncLE'ToRestrictionNatTrans
- ComplexShape.Embedding.mem_prev
- HomologicalComplex.shortComplexTruncLE_shortExact_δ_eq_zero
- HomologicalComplex.isIso_homologyMap_shortComplexTruncLE_g
- HomologicalComplex.mono_homologyMap_shortComplexTruncLE_g
- HomologicalComplex.quasiIso_truncLEMap_iff
- ComplexShape.Embedding.ιTruncLENatTrans
- HomologicalComplex.truncLE'ToRestriction_naturality
- HomologicalComplex.isIso_ιTruncLE_iff
- HomologicalComplex.truncLEMap_comp
- ComplexShape.Embedding.IsTruncLE.mem_prev
- HomologicalComplex.truncLE'Map_comp
- HomologicalComplex.quasiIsoAt_ιTruncLE
- HomologicalComplex.instIsIsoFTruncLE'ToRestrictionOfIsStrictlySupported
- HomologicalComplex.instMonoFShortComplexTruncLE
- HomologicalComplex.epi_homologyMap_shortComplexTruncLE_g
- HomologicalComplex.truncLEXIsoCycles
- ComplexShape.Embedding.truncLEFunctor_map
- HomologicalComplex.instMonoιTruncLE
- HomologicalComplex.shortComplexTruncLE_X₃_isSupportedOutside
- HomologicalComplex.shortComplexTruncLEX₃ToTruncGE.congr_simp
- HomologicalComplex.instIsStrictlySupportedTruncLE
- HomologicalComplex.truncLE'.truncLE'_hasHomology
- ComplexShape.Embedding.IsTruncLE.toIsRelIff
- ComplexShape.Embedding.truncLEFunctor.congr_simp
- ComplexShape.Embedding.instIsTruncGEOpOfIsTruncLE
- HomologicalComplex.truncLEXIso
- HomologicalComplex.truncLEIso
- HomologicalComplex.instMonoFTruncLE'ToRestriction
- ComplexShape.Embedding.BoundaryGE.false_of_isTruncLE
- ComplexShape.Embedding.truncLE'Functor_obj
- ComplexShape.Embedding.truncLE'Functor.congr_simp
- HomologicalComplex.truncLEMap_id