BddOrd

📁 Source: Mathlib/Order/Category/BddOrd.lean

Statistics

Metric	Count
Definitions BddOrd, hom, hom, hom', mk, dual, dualEquiv, hasForgetToBipointed, hasForgetToPartOrd, instCategory, instCoeSortType, instConcreteCategoryBoundedOrderHomCarrier, instInhabited, isBoundedOrder, of, ofHom, toPartOrd	17
Theorems ext, ext_iff, mk_hom, mk_inv, coe_comp, coe_id, coe_of, comp_apply, dualEquiv_functor, dualEquiv_inverse, dual_map, ext, ext_iff, forget_map, hom_comp, hom_ext, hom_ext_iff, hom_id, hom_inv_apply, hom_ofHom, id_apply, inv_hom_apply, ofHom_apply, ofHom_comp, ofHom_hom, ofHom_id, bddOrd_dual_comp_forget_to_bipointed, bddOrd_dual_comp_forget_to_partOrd	28
Total	45

BddOrd

Definitions

Name	Category	Theorems
dual 📖	CompOp	6 math math: bddOrd_dual_comp_forget_to_bipointed, dualEquiv_functor, dual_map, bddOrd_dual_comp_forget_to_partOrd, bddLat_dual_comp_forget_to_bddOrd, dualEquiv_inverse
dualEquiv 📖	CompOp	2 math math: dualEquiv_functor, dualEquiv_inverse
hasForgetToBipointed 📖	CompOp	1 math math: bddOrd_dual_comp_forget_to_bipointed
hasForgetToPartOrd 📖	CompOp	4 math math: BddLat.forget_semilatSup_partOrd_eq_forget_bddOrd_partOrd, BddLat.forget_semilatInf_partOrd_eq_forget_bddOrd_partOrd, bddOrd_dual_comp_forget_to_partOrd, BddLat.forget_lat_partOrd_eq_forget_bddOrd_partOrd
instCategory 📖	CompOp	25 math math: bddOrd_dual_comp_forget_to_bipointed, dualEquiv_functor, coe_id, hom_id, ext_iff, BddLat.forget_semilatSup_partOrd_eq_forget_bddOrd_partOrd, Iso.mk_hom, dual_map, BddLat.forget_semilatInf_partOrd_eq_forget_bddOrd_partOrd, bddOrd_dual_comp_forget_to_partOrd, forget_map, id_apply, bddLat_dual_comp_forget_to_bddOrd, BddLat.forget_lat_partOrd_eq_forget_bddOrd_partOrd, Iso.mk_inv, hom_comp, hom_inv_apply, comp_apply, BddLat.coe_forget_to_bddOrd, ofHom_apply, ofHom_comp, ofHom_id, coe_comp, inv_hom_apply, dualEquiv_inverse
instCoeSortType 📖	CompOp	—
instConcreteCategoryBoundedOrderHomCarrier 📖	CompOp	16 math math: bddOrd_dual_comp_forget_to_bipointed, coe_id, ext_iff, BddLat.forget_semilatSup_partOrd_eq_forget_bddOrd_partOrd, BddLat.forget_semilatInf_partOrd_eq_forget_bddOrd_partOrd, bddOrd_dual_comp_forget_to_partOrd, forget_map, id_apply, bddLat_dual_comp_forget_to_bddOrd, BddLat.forget_lat_partOrd_eq_forget_bddOrd_partOrd, hom_inv_apply, comp_apply, BddLat.coe_forget_to_bddOrd, ofHom_apply, coe_comp, inv_hom_apply
instInhabited 📖	CompOp	—
isBoundedOrder 📖	CompOp	22 math math: bddOrd_dual_comp_forget_to_bipointed, coe_id, hom_id, ext_iff, BddLat.forget_semilatSup_partOrd_eq_forget_bddOrd_partOrd, Iso.mk_hom, dual_map, BddLat.forget_semilatInf_partOrd_eq_forget_bddOrd_partOrd, bddOrd_dual_comp_forget_to_partOrd, forget_map, id_apply, bddLat_dual_comp_forget_to_bddOrd, BddLat.forget_lat_partOrd_eq_forget_bddOrd_partOrd, Iso.mk_inv, hom_comp, hom_inv_apply, comp_apply, BddLat.coe_forget_to_bddOrd, ofHom_apply, ofHom_hom, coe_comp, inv_hom_apply
of 📖	CompOp	5 math math: hom_ofHom, coe_of, ofHom_apply, ofHom_comp, ofHom_id
ofHom 📖	CompOp	8 math math: Iso.mk_hom, dual_map, hom_ofHom, Iso.mk_inv, ofHom_apply, ofHom_comp, ofHom_id, ofHom_hom
toPartOrd 📖	CompOp	23 math math: bddOrd_dual_comp_forget_to_bipointed, coe_id, hom_id, ext_iff, BddLat.forget_semilatSup_partOrd_eq_forget_bddOrd_partOrd, Iso.mk_hom, dual_map, BddLat.forget_semilatInf_partOrd_eq_forget_bddOrd_partOrd, bddOrd_dual_comp_forget_to_partOrd, forget_map, id_apply, coe_of, bddLat_dual_comp_forget_to_bddOrd, BddLat.forget_lat_partOrd_eq_forget_bddOrd_partOrd, Iso.mk_inv, hom_comp, hom_inv_apply, comp_apply, BddLat.coe_forget_to_bddOrd, ofHom_apply, ofHom_hom, coe_comp, inv_hom_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_comp 📖	mathematical	—	DFunLike.coe CategoryTheory.ConcreteCategory.hom BddOrd instCategory BoundedOrderHom PartOrd.carrier toPartOrd PartialOrder.toPreorder PartOrd.str isBoundedOrder BoundedOrderHom.instFunLike instConcreteCategoryBoundedOrderHomCarrier CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	—
coe_id 📖	mathematical	—	DFunLike.coe CategoryTheory.ConcreteCategory.hom BddOrd instCategory BoundedOrderHom PartOrd.carrier toPartOrd PartialOrder.toPreorder PartOrd.str isBoundedOrder BoundedOrderHom.instFunLike instConcreteCategoryBoundedOrderHomCarrier CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
coe_of 📖	mathematical	—	PartOrd.carrier toPartOrd of	—	—
comp_apply 📖	mathematical	—	DFunLike.coe CategoryTheory.ConcreteCategory.hom BddOrd instCategory BoundedOrderHom PartOrd.carrier toPartOrd PartialOrder.toPreorder PartOrd.str isBoundedOrder BoundedOrderHom.instFunLike instConcreteCategoryBoundedOrderHomCarrier CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	—
dualEquiv_functor 📖	mathematical	—	CategoryTheory.Equivalence.functor BddOrd instCategory dualEquiv dual	—	—
dualEquiv_inverse 📖	mathematical	—	CategoryTheory.Equivalence.inverse BddOrd instCategory dualEquiv dual	—	—
dual_map 📖	mathematical	—	CategoryTheory.Functor.map BddOrd instCategory dual ofHom OrderDual PartOrd.carrier toPartOrd OrderDual.instPartialOrder PartOrd.str OrderDual.instBoundedOrder Preorder.toLE PartialOrder.toPreorder isBoundedOrder DFunLike.coe Equiv BoundedOrderHom OrderDual.instPreorder EquivLike.toFunLike Equiv.instEquivLike BoundedOrderHom.dual Hom.hom	—	—
ext 📖	—	DFunLike.coe CategoryTheory.ConcreteCategory.hom BddOrd instCategory BoundedOrderHom PartOrd.carrier toPartOrd PartialOrder.toPreorder PartOrd.str isBoundedOrder BoundedOrderHom.instFunLike instConcreteCategoryBoundedOrderHomCarrier	—	—	CategoryTheory.ConcreteCategory.hom_ext
ext_iff 📖	mathematical	—	DFunLike.coe CategoryTheory.ConcreteCategory.hom BddOrd instCategory BoundedOrderHom PartOrd.carrier toPartOrd PartialOrder.toPreorder PartOrd.str isBoundedOrder BoundedOrderHom.instFunLike instConcreteCategoryBoundedOrderHomCarrier	—	ext
forget_map 📖	mathematical	—	CategoryTheory.Functor.map BddOrd instCategory CategoryTheory.types CategoryTheory.forget BoundedOrderHom PartOrd.carrier toPartOrd PartialOrder.toPreorder PartOrd.str isBoundedOrder BoundedOrderHom.instFunLike instConcreteCategoryBoundedOrderHomCarrier DFunLike.coe CategoryTheory.ConcreteCategory.hom	—	—
hom_comp 📖	mathematical	—	Hom.hom CategoryTheory.CategoryStruct.comp BddOrd CategoryTheory.Category.toCategoryStruct instCategory BoundedOrderHom.comp PartOrd.carrier toPartOrd PartialOrder.toPreorder PartOrd.str isBoundedOrder	—	—
hom_ext 📖	—	Hom.hom	—	—	Hom.ext
hom_ext_iff 📖	mathematical	—	Hom.hom	—	hom_ext
hom_id 📖	mathematical	—	Hom.hom CategoryTheory.CategoryStruct.id BddOrd CategoryTheory.Category.toCategoryStruct instCategory BoundedOrderHom.id PartOrd.carrier toPartOrd PartialOrder.toPreorder PartOrd.str isBoundedOrder	—	—
hom_inv_apply 📖	mathematical	—	DFunLike.coe CategoryTheory.ConcreteCategory.hom BddOrd instCategory BoundedOrderHom PartOrd.carrier toPartOrd PartialOrder.toPreorder PartOrd.str isBoundedOrder BoundedOrderHom.instFunLike instConcreteCategoryBoundedOrderHomCarrier CategoryTheory.Iso.hom CategoryTheory.Iso.inv	—	CategoryTheory.Iso.inv_hom_id_apply
hom_ofHom 📖	mathematical	—	Hom.hom of ofHom	—	—
id_apply 📖	mathematical	—	DFunLike.coe CategoryTheory.ConcreteCategory.hom BddOrd instCategory BoundedOrderHom PartOrd.carrier toPartOrd PartialOrder.toPreorder PartOrd.str isBoundedOrder BoundedOrderHom.instFunLike instConcreteCategoryBoundedOrderHomCarrier CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
inv_hom_apply 📖	mathematical	—	DFunLike.coe CategoryTheory.ConcreteCategory.hom BddOrd instCategory BoundedOrderHom PartOrd.carrier toPartOrd PartialOrder.toPreorder PartOrd.str isBoundedOrder BoundedOrderHom.instFunLike instConcreteCategoryBoundedOrderHomCarrier CategoryTheory.Iso.inv CategoryTheory.Iso.hom	—	CategoryTheory.Iso.hom_inv_id_apply
ofHom_apply 📖	mathematical	—	DFunLike.coe of CategoryTheory.ConcreteCategory.hom BddOrd instCategory BoundedOrderHom PartOrd.carrier toPartOrd PartialOrder.toPreorder PartOrd.str isBoundedOrder BoundedOrderHom.instFunLike instConcreteCategoryBoundedOrderHomCarrier ofHom	—	—
ofHom_comp 📖	mathematical	—	ofHom BoundedOrderHom.comp PartialOrder.toPreorder CategoryTheory.CategoryStruct.comp BddOrd CategoryTheory.Category.toCategoryStruct instCategory of	—	—
ofHom_hom 📖	mathematical	—	ofHom PartOrd.carrier toPartOrd PartOrd.str isBoundedOrder Hom.hom	—	—
ofHom_id 📖	mathematical	—	ofHom BoundedOrderHom.id PartialOrder.toPreorder CategoryTheory.CategoryStruct.id BddOrd CategoryTheory.Category.toCategoryStruct instCategory of	—	—

BddOrd.Hom

Definitions

Name	Category	Theorems
hom 📖	CompOp	6 math math: BddOrd.hom_id, BddOrd.dual_map, BddOrd.hom_ofHom, BddOrd.hom_comp, BddOrd.hom_ext_iff, BddOrd.ofHom_hom
hom' 📖	CompOp	1 math math: ext_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	hom'	—	—	—
ext_iff 📖	mathematical	—	hom'	—	ext

BddOrd.Hom.Simps

Definitions

Name	Category	Theorems
hom 📖	CompOp	—

BddOrd.Iso

Definitions

Name	Category	Theorems
mk 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mk_hom 📖	mathematical	—	CategoryTheory.Iso.hom BddOrd BddOrd.instCategory BddOrd.ofHom PartOrd.carrier PartOrd.str BddOrd.isBoundedOrder BoundedOrderHomClass.toBoundedOrderHom OrderIso BddOrd.toPartOrd Preorder.toLE PartialOrder.toPreorder instFunLikeOrderIso	—	—
mk_inv 📖	mathematical	—	CategoryTheory.Iso.inv BddOrd BddOrd.instCategory BddOrd.ofHom PartOrd.carrier PartOrd.str BddOrd.isBoundedOrder BoundedOrderHomClass.toBoundedOrderHom OrderIso BddOrd.toPartOrd Preorder.toLE PartialOrder.toPreorder instFunLikeOrderIso OrderIso.symm	—	—

(root)

Definitions

Name	Category	Theorems
BddOrd 📖	CompData	25 math math: bddOrd_dual_comp_forget_to_bipointed, BddOrd.dualEquiv_functor, BddOrd.coe_id, BddOrd.hom_id, BddOrd.ext_iff, BddLat.forget_semilatSup_partOrd_eq_forget_bddOrd_partOrd, BddOrd.Iso.mk_hom, BddOrd.dual_map, BddLat.forget_semilatInf_partOrd_eq_forget_bddOrd_partOrd, bddOrd_dual_comp_forget_to_partOrd, BddOrd.forget_map, BddOrd.id_apply, bddLat_dual_comp_forget_to_bddOrd, BddLat.forget_lat_partOrd_eq_forget_bddOrd_partOrd, BddOrd.Iso.mk_inv, BddOrd.hom_comp, BddOrd.hom_inv_apply, BddOrd.comp_apply, BddLat.coe_forget_to_bddOrd, BddOrd.ofHom_apply, BddOrd.ofHom_comp, BddOrd.ofHom_id, BddOrd.coe_comp, BddOrd.inv_hom_apply, BddOrd.dualEquiv_inverse

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bddOrd_dual_comp_forget_to_bipointed 📖	mathematical	—	CategoryTheory.Functor.comp BddOrd BddOrd.instCategory Bipointed Bipointed.largeCategory BddOrd.dual CategoryTheory.forget₂ BoundedOrderHom PartOrd.carrier BddOrd.toPartOrd PartialOrder.toPreorder PartOrd.str BddOrd.isBoundedOrder BoundedOrderHom.instFunLike BddOrd.instConcreteCategoryBoundedOrderHomCarrier Bipointed.HomSubtype Bipointed.X Bipointed.instFunLikeHomSubtypeX Bipointed.hasForget BddOrd.hasForgetToBipointed Bipointed.swap	—	—
bddOrd_dual_comp_forget_to_partOrd 📖	mathematical	—	CategoryTheory.Functor.comp BddOrd BddOrd.instCategory PartOrd PartOrd.instCategory BddOrd.dual CategoryTheory.forget₂ BoundedOrderHom PartOrd.carrier BddOrd.toPartOrd PartialOrder.toPreorder PartOrd.str BddOrd.isBoundedOrder BoundedOrderHom.instFunLike BddOrd.instConcreteCategoryBoundedOrderHomCarrier OrderHom OrderHom.instFunLike PartOrd.instConcreteCategoryOrderHomCarrier BddOrd.hasForgetToPartOrd PartOrd.dual	—	—

---

← Back to Index