WithBotTop

📁 Source: Mathlib/Order/WithBotTop.lean

Statistics

Metric	Count
Definitions EInt, WithBotTop, instCoe, rec	4
Theorems coe_injective, coe_le_coe, coe_lt_coe, coe_monotone, coe_ne_bot, coe_ne_top, coe_strictMono, rec_bot, rec_coe, rec_top, top_ne_bot	11
Total	15

WithBotTop

Definitions

Name	Category	Theorems
instCoe 📖	CompOp	—
rec 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_injective 📖	mathematical	—	WithBotTop coe	—	—
coe_le_coe 📖	mathematical	—	WithBotTop WithBot.instLE WithTop WithTop.instLE coe	—	WithTop.coe_le_coe WithBot.coe_le_coe
coe_lt_coe 📖	mathematical	—	WithBotTop WithBot.instLT WithTop WithTop.instLT coe	—	WithTop.coe_lt_coe WithBot.coe_lt_coe
coe_monotone 📖	mathematical	—	Monotone WithBotTop WithBot.instPreorder WithTop WithTop.instPreorder coe	—	—
coe_ne_bot 📖	—	—	—	—	—
coe_ne_top 📖	—	—	—	—	—
coe_strictMono 📖	mathematical	—	StrictMono WithBotTop WithBot.instPreorder WithTop WithTop.instPreorder coe	—	StrictMono.comp WithBot.coe_strictMono WithTop.coe_strictMono
rec_bot 📖	mathematical	—	Bot.bot WithBotTop WithBot.bot WithTop	—	—
rec_coe 📖	mathematical	—	coe	—	—
rec_top 📖	mathematical	—	Top.top WithBotTop WithBot.instTop WithTop WithTop.top	—	—
top_ne_bot 📖	—	—	—	—	—

(root)

Definitions

Name	Category	Theorems
EInt 📖	CompOp	127 math math: CategoryTheory.Triangulated.TStructure.eTruncLT_map_app_eTruncLTι_app, CategoryTheory.Triangulated.TStructure.eTriangleLTGE_map_app_hom₃, CategoryTheory.Abelian.SpectralObject.coreE₂HomologicalNat_deg, CategoryTheory.Triangulated.TStructure.triangleω₁δ_obj_mor₁, CategoryTheory.Triangulated.TStructure.eTriangleLTGE_map_app_hom₂, CategoryTheory.Triangulated.TStructure.eTruncGEπ_naturality_assoc, CategoryTheory.Triangulated.TStructure.triangleω₁δ_obj_obj₂, CategoryTheory.Triangulated.TStructure.eTruncLTLTIsoLT_inv_hom_id_app, CategoryTheory.Abelian.SpectralObject.coreE₂Cohomological_i₃, CategoryTheory.Triangulated.TStructure.instIsIsoMapObjEIntFunctorETruncLTAppETruncLTι, CategoryTheory.Abelian.SpectralObject.instHasSpectralSequenceEIntProdIntCoreE₂Cohomological, CategoryTheory.Triangulated.TStructure.eTruncLTGELTSelfToLTGE_app, CategoryTheory.Triangulated.TStructure.isIso_eTruncGE_obj_map_truncGEπ_app, CategoryTheory.Triangulated.TStructure.eTruncLTLTToLT_app, CategoryTheory.Triangulated.TStructure.triangleω₁δ_map_hom₁, CategoryTheory.Triangulated.TStructure.eTruncGEπ_bot, CategoryTheory.Triangulated.TStructure.ω₁δ_naturality_assoc, CategoryTheory.Triangulated.TStructure.eTruncGEIsoGEGE_hom_inv_id_app_assoc, CategoryTheory.Triangulated.TStructure.instAdditiveObjEIntFunctorETruncLT, CategoryTheory.Triangulated.TStructure.triangleω₁δ_map_hom₂, CategoryTheory.Triangulated.TStructure.eTruncLTLTIsoLT_inv_hom_id_app_eTruncLT_obj, CategoryTheory.Triangulated.TStructure.spectralObject_ω₁, CategoryTheory.Triangulated.TStructure.eTriangleLTGE_obj_obj_obj₁, CategoryTheory.Triangulated.TStructure.ω₁_map, CategoryTheory.Triangulated.TStructure.eTruncGEπ_naturality, CategoryTheory.Abelian.SpectralObject.IsFirstQuadrant.isZero₂, CategoryTheory.Triangulated.TStructure.isZero_eTruncGE_obj_obj, CategoryTheory.Triangulated.TStructure.eTruncLTGEIsoGELT_hom_app_fac, CategoryTheory.Triangulated.TStructure.instIsIsoFunctorETruncLTGELTSelfToGELT, CategoryTheory.Triangulated.TStructure.eTruncLTLTIsoLT_inv_hom_id_app_eTruncLT_obj_assoc, CategoryTheory.Triangulated.TStructure.eTriangleLTGE_obj_obj_mor₁, CategoryTheory.Triangulated.TStructure.eTruncGEIsoGEGE_inv_hom_id_app_assoc, CategoryTheory.Abelian.SpectralObject.coreE₂HomologicalNat_i₂, CategoryTheory.Triangulated.TStructure.triangleω₁δ_map_hom₃, CategoryTheory.Abelian.SpectralObject.instHasSpectralSequenceEIntProdNatCoreE₂HomologicalNat, CategoryTheory.Triangulated.TStructure.instIsGEObjEIntFunctorETruncGE, CategoryTheory.Abelian.SpectralObject.isZero₁_of_isFirstQuadrant, CategoryTheory.Triangulated.TStructure.eTruncGEπ_top, CategoryTheory.Triangulated.TStructure.instIsIsoFunctorETruncLTιTopEInt, CategoryTheory.Abelian.SpectralObject.isZero₁_of_isThirdQuadrant, CategoryTheory.Triangulated.TStructure.eTruncLTGEIsoGELT_hom_app_fac'_assoc, CategoryTheory.Triangulated.TStructure.eTruncLTGEIsoGELT_hom_app_fac_assoc, CategoryTheory.Triangulated.TStructure.eTruncLT_obj_coe, CategoryTheory.Triangulated.TStructure.eTruncLTLTIsoLT_hom_inv_id_app, CategoryTheory.Triangulated.TStructure.spectralObjectFunctor_map_hom, CategoryTheory.Abelian.SpectralObject.coreE₂CohomologicalNat_i₂, CategoryTheory.Triangulated.TStructure.eTruncGEπ_app_eTruncGE_map_app_assoc, CategoryTheory.Abelian.SpectralObject.coreE₂CohomologicalNat_deg, CategoryTheory.Triangulated.TStructure.eTruncLT_obj_map_eTruncLTι_app, CategoryTheory.Triangulated.TStructure.eTruncLTLTIsoLT_inv_hom_id_app_assoc, CategoryTheory.Triangulated.TStructure.eTriangleLTGE_map_app_hom₁, CategoryTheory.Abelian.SpectralObject.isZero₂_of_isFirstQuadrant, CategoryTheory.Abelian.SpectralObject.IsFirstQuadrant.isZero₁, CategoryTheory.Triangulated.TStructure.eTruncLT_ι_top, CategoryTheory.Triangulated.TStructure.eTruncLT_obj_bot, CategoryTheory.Triangulated.TStructure.ω₁_obj, CategoryTheory.Abelian.SpectralObject.coreE₂Cohomological_i₂, CategoryTheory.Abelian.SpectralObject.IsThirdQuadrant.isZero₂, CategoryTheory.Triangulated.TStructure.eTruncLTι_naturality, CategoryTheory.Triangulated.TStructure.eTriangleLTGE_obj_map_hom₃, CategoryTheory.Triangulated.TStructure.isIso_eTruncLT_obj_map_truncLTπ_app, CategoryTheory.Abelian.SpectralObject.coreE₂HomologicalNat_i₀, CategoryTheory.Triangulated.TStructure.eTruncGE_obj_map_eTruncGEπ_app_assoc, CategoryTheory.Abelian.SpectralObject.coreE₂HomologicalNat_i₁, CategoryTheory.Triangulated.TStructure.eTruncLT_obj_map_eTruncLTι_app_assoc, CategoryTheory.Triangulated.TStructure.isIso_eTruncLTLTIsoLT, CategoryTheory.Triangulated.TStructure.eTruncLTGELTSelfToGELT_app, CategoryTheory.Abelian.SpectralObject.coreE₂CohomologicalNat_i₁, CategoryTheory.Triangulated.TStructure.eTruncLTGEIsoGELT_naturality_app_assoc, CategoryTheory.Triangulated.TStructure.eTruncGE_obj_map_eTruncGEπ_app, CategoryTheory.Triangulated.TStructure.eTriangleLTGE_distinguished, CategoryTheory.Triangulated.TStructure.isLE_eTruncLT_obj_obj, CategoryTheory.Abelian.SpectralObject.coreE₂Cohomological_deg, CategoryTheory.Triangulated.TStructure.spectralObjectFunctor_obj, CategoryTheory.Triangulated.TStructure.triangleω₁δ_obj_obj₁, CategoryTheory.Triangulated.TStructure.eTruncLT_map_app_eTruncLTι_app_assoc, CategoryTheory.Triangulated.TStructure.eTruncGEIsoGEGE_hom_inv_id_app, CategoryTheory.Triangulated.TStructure.eTruncGEIsoGEGE_hom, CategoryTheory.Triangulated.TStructure.ω₁δ_app, CategoryTheory.Triangulated.TStructure.triangleω₁δ_obj_mor₃, CategoryTheory.Triangulated.TStructure.eTruncGEπ_app_eTruncGE_map_app, CategoryTheory.Triangulated.TStructure.isIso_eTruncGEIsoGEGE, CategoryTheory.Triangulated.TStructure.eTruncGEIsoGEGE_inv_hom_id_app, CategoryTheory.Triangulated.TStructure.eTruncLTLTIsoLT_hom_inv_id_app_assoc, CategoryTheory.Abelian.SpectralObject.coreE₂HomologicalNat_i₃, CategoryTheory.Triangulated.TStructure.eTruncGE_obj_top, CategoryTheory.Triangulated.TStructure.eTruncLTGEIsoGELT_hom_app_fac', CategoryTheory.Triangulated.TStructure.instIsIsoFunctorETruncLTGELTSelfToLTGE, CategoryTheory.Triangulated.TStructure.eTruncLTGEIsoGELT_naturality_app, CategoryTheory.Triangulated.TStructure.eTruncLT_obj_map_eTruncLTι_app_eTruncLT_map_app_assoc, CategoryTheory.Triangulated.TStructure.instIsLEObjEIntFunctorETruncGE, CategoryTheory.Triangulated.TStructure.instIsIsoFunctorETruncGEπBotEInt, CategoryTheory.Triangulated.TStructure.eTriangleLTGE_obj_obj_mor₃, CategoryTheory.Triangulated.TStructure.eTruncLTι_naturality_assoc, CategoryTheory.Triangulated.TStructure.isZero_eTruncLT_obj_obj, CategoryTheory.Triangulated.TStructure.eTruncGE_obj_coe, CategoryTheory.Abelian.SpectralObject.coreE₂Cohomological_i₀, CategoryTheory.Triangulated.TStructure.eTriangleLTGE_obj_obj_obj₂, CategoryTheory.Triangulated.TStructure.instIsGEObjEIntFunctorETruncLT, CategoryTheory.Triangulated.TStructure.eTruncLT_ι_bot, CategoryTheory.Triangulated.TStructure.triangleω₁δ_obj_mor₂, CategoryTheory.Triangulated.TStructure.eTruncGEδLT_coe, CategoryTheory.Abelian.SpectralObject.isZero₂_of_isThirdQuadrant, CategoryTheory.Abelian.SpectralObject.coreE₂CohomologicalNat_i₀, CategoryTheory.Triangulated.TStructure.instAdditiveObjEIntFunctorETruncGE, CategoryTheory.Triangulated.TStructure.ω₁δ_naturality, CategoryTheory.Triangulated.TStructure.instIsIsoAppETruncLTιObjEIntFunctorETruncLT, CategoryTheory.Triangulated.TStructure.isGE_eTruncGE_obj_obj, CategoryTheory.Triangulated.TStructure.eTruncLT_obj_top, CategoryTheory.Triangulated.TStructure.instIsLEObjEIntFunctorETruncLT, CategoryTheory.Triangulated.TStructure.eTruncLTGEIsoGELT_hom_naturality_assoc, CategoryTheory.Triangulated.TStructure.eTruncLT_obj_map_eTruncLTι_app_eTruncLT_map_app, CategoryTheory.Triangulated.TStructure.eTruncGE_obj_bot, CategoryTheory.Triangulated.TStructure.triangleω₁δ_obj_obj₃, CategoryTheory.Abelian.SpectralObject.coreE₂Cohomological_i₁, CategoryTheory.Triangulated.TStructure.eTriangleLTGE_obj_obj_obj₃, CategoryTheory.Triangulated.TStructure.eTruncLTLTIsoLT_hom, CategoryTheory.Abelian.SpectralObject.coreE₂CohomologicalNat_i₃, CategoryTheory.Abelian.SpectralObject.IsThirdQuadrant.isZero₁, CategoryTheory.Triangulated.TStructure.eTriangleLTGE_obj_map_hom₂, CategoryTheory.Triangulated.TStructure.eTriangleLTGE_obj_map_hom₁, CategoryTheory.Triangulated.TStructure.eTriangleLTGE_obj_obj_mor₂, CategoryTheory.Triangulated.TStructure.eTruncLTGEIsoGELT_hom_naturality, CategoryTheory.Triangulated.TStructure.eTruncGEToGEGE_app, CategoryTheory.Triangulated.TStructure.eTruncLT_map_eq_truncLTι, CategoryTheory.Abelian.SpectralObject.instHasSpectralSequenceEIntProdNatCoreE₂CohomologicalNat, CategoryTheory.Triangulated.TStructure.spectralObject_δ
WithBotTop 📖	CompOp	8 math math: WithBotTop.coe_strictMono, WithBotTop.rec_bot, WithBotTop.coe_le_coe, WithBotTop.coe_monotone, WithBotTop.rec_top, WithBotTop.coe_injective, WithBotTop.coe_lt_coe, CategoryTheory.Triangulated.TStructure.eTruncLT_map_eq_truncLTι

---

← Back to Index