FinBddDistLat

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

Statistics

Metric	Count
Definitions FinBddDistLat, hom, hom, hom', mk, dual, dualEquiv, hasForgetToBddDistLat, hasForgetToFinPartOrd, instBoundedOrderCarrier, instCategory, instCoeSortType, instConcreteCategoryBoundedLatticeHomCarrier, instDistribLatticeCarrier, instInhabited, isFintype, of, of', ofHom, toBddDistLat	20
Theorems ext, ext_iff, mk_hom, mk_inv, coe_comp, coe_id, 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, finBddDistLat_dual_comp_forget_to_bddDistLat	26
Total	46

FinBddDistLat

Definitions

Name	Category	Theorems
dual 📖	CompOp	5 math math: dualEquiv_functor, finBddDistLat_dual_comp_forget_to_bddDistLat, finBoolAlg_dual_comp_forget_to_finBddDistLat, dual_map, dualEquiv_inverse
dualEquiv 📖	CompOp	2 math math: dualEquiv_functor, dualEquiv_inverse
hasForgetToBddDistLat 📖	CompOp	1 math math: finBddDistLat_dual_comp_forget_to_bddDistLat
hasForgetToFinPartOrd 📖	CompOp	—
instBoundedOrderCarrier 📖	CompOp	15 math math: ofHom_apply, hom_inv_apply, ext_iff, coe_id, inv_hom_apply, finBddDistLat_dual_comp_forget_to_bddDistLat, forget_map, comp_apply, ofHom_hom, finBoolAlg_dual_comp_forget_to_finBddDistLat, hom_comp, coe_comp, id_apply, hom_id, dual_map
instCategory 📖	CompOp	20 math math: ofHom_comp, ofHom_apply, dualEquiv_functor, hom_inv_apply, ext_iff, coe_id, inv_hom_apply, finBddDistLat_dual_comp_forget_to_bddDistLat, forget_map, comp_apply, finBoolAlg_dual_comp_forget_to_finBddDistLat, hom_comp, coe_comp, Iso.mk_inv, id_apply, hom_id, dual_map, dualEquiv_inverse, ofHom_id, Iso.mk_hom
instCoeSortType 📖	CompOp	—
instConcreteCategoryBoundedLatticeHomCarrier 📖	CompOp	11 math math: ofHom_apply, hom_inv_apply, ext_iff, coe_id, inv_hom_apply, finBddDistLat_dual_comp_forget_to_bddDistLat, forget_map, comp_apply, finBoolAlg_dual_comp_forget_to_finBddDistLat, coe_comp, id_apply
instDistribLatticeCarrier 📖	CompOp	15 math math: ofHom_apply, hom_inv_apply, ext_iff, coe_id, inv_hom_apply, finBddDistLat_dual_comp_forget_to_bddDistLat, forget_map, comp_apply, ofHom_hom, finBoolAlg_dual_comp_forget_to_finBddDistLat, hom_comp, coe_comp, id_apply, hom_id, dual_map
instInhabited 📖	CompOp	—
isFintype 📖	CompOp	4 math math: ofHom_hom, Iso.mk_inv, dual_map, Iso.mk_hom
of 📖	CompOp	4 math math: ofHom_comp, ofHom_apply, hom_ofHom, ofHom_id
of' 📖	CompOp	—
ofHom 📖	CompOp	8 math math: ofHom_comp, ofHom_apply, ofHom_hom, hom_ofHom, Iso.mk_inv, dual_map, ofHom_id, Iso.mk_hom
toBddDistLat 📖	CompOp	15 math math: ofHom_apply, hom_inv_apply, ext_iff, coe_id, inv_hom_apply, finBddDistLat_dual_comp_forget_to_bddDistLat, forget_map, comp_apply, ofHom_hom, finBoolAlg_dual_comp_forget_to_finBddDistLat, hom_comp, coe_comp, id_apply, hom_id, dual_map

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_comp 📖	mathematical	—	DFunLike.coe CategoryTheory.ConcreteCategory.hom FinBddDistLat instCategory BoundedLatticeHom DistLat.carrier BddDistLat.toDistLat toBddDistLat DistribLattice.toLattice instDistribLatticeCarrier instBoundedOrderCarrier BoundedLatticeHom.instFunLike instConcreteCategoryBoundedLatticeHomCarrier CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	—
coe_id 📖	mathematical	—	DFunLike.coe CategoryTheory.ConcreteCategory.hom FinBddDistLat instCategory BoundedLatticeHom DistLat.carrier BddDistLat.toDistLat toBddDistLat DistribLattice.toLattice instDistribLatticeCarrier instBoundedOrderCarrier BoundedLatticeHom.instFunLike instConcreteCategoryBoundedLatticeHomCarrier CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
comp_apply 📖	mathematical	—	DFunLike.coe CategoryTheory.ConcreteCategory.hom FinBddDistLat instCategory BoundedLatticeHom DistLat.carrier BddDistLat.toDistLat toBddDistLat DistribLattice.toLattice instDistribLatticeCarrier instBoundedOrderCarrier BoundedLatticeHom.instFunLike instConcreteCategoryBoundedLatticeHomCarrier CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	—
dualEquiv_functor 📖	mathematical	—	CategoryTheory.Equivalence.functor FinBddDistLat instCategory dualEquiv dual	—	—
dualEquiv_inverse 📖	mathematical	—	CategoryTheory.Equivalence.inverse FinBddDistLat instCategory dualEquiv dual	—	—
dual_map 📖	mathematical	—	CategoryTheory.Functor.map FinBddDistLat instCategory dual ofHom OrderDual DistLat.carrier BddDistLat.toDistLat toBddDistLat OrderDual.instDistribLattice instDistribLatticeCarrier OrderDual.instBoundedOrder Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instBoundedOrderCarrier OrderDual.fintype isFintype DFunLike.coe Equiv BoundedLatticeHom OrderDual.instLattice EquivLike.toFunLike Equiv.instEquivLike BoundedLatticeHom.dual Hom.hom	—	—
ext 📖	—	DFunLike.coe CategoryTheory.ConcreteCategory.hom FinBddDistLat instCategory BoundedLatticeHom DistLat.carrier BddDistLat.toDistLat toBddDistLat DistribLattice.toLattice instDistribLatticeCarrier instBoundedOrderCarrier BoundedLatticeHom.instFunLike instConcreteCategoryBoundedLatticeHomCarrier	—	—	CategoryTheory.ConcreteCategory.hom_ext
ext_iff 📖	mathematical	—	DFunLike.coe CategoryTheory.ConcreteCategory.hom FinBddDistLat instCategory BoundedLatticeHom DistLat.carrier BddDistLat.toDistLat toBddDistLat DistribLattice.toLattice instDistribLatticeCarrier instBoundedOrderCarrier BoundedLatticeHom.instFunLike instConcreteCategoryBoundedLatticeHomCarrier	—	ext
forget_map 📖	mathematical	—	CategoryTheory.Functor.map FinBddDistLat instCategory CategoryTheory.types CategoryTheory.forget BoundedLatticeHom DistLat.carrier BddDistLat.toDistLat toBddDistLat DistribLattice.toLattice instDistribLatticeCarrier instBoundedOrderCarrier BoundedLatticeHom.instFunLike instConcreteCategoryBoundedLatticeHomCarrier DFunLike.coe CategoryTheory.ConcreteCategory.hom	—	—
hom_comp 📖	mathematical	—	Hom.hom CategoryTheory.CategoryStruct.comp FinBddDistLat CategoryTheory.Category.toCategoryStruct instCategory BoundedLatticeHom.comp DistLat.carrier BddDistLat.toDistLat toBddDistLat DistribLattice.toLattice instDistribLatticeCarrier instBoundedOrderCarrier	—	—
hom_ext 📖	—	Hom.hom	—	—	Hom.ext
hom_ext_iff 📖	mathematical	—	Hom.hom	—	hom_ext
hom_id 📖	mathematical	—	Hom.hom CategoryTheory.CategoryStruct.id FinBddDistLat CategoryTheory.Category.toCategoryStruct instCategory BoundedLatticeHom.id DistLat.carrier BddDistLat.toDistLat toBddDistLat DistribLattice.toLattice instDistribLatticeCarrier instBoundedOrderCarrier	—	—
hom_inv_apply 📖	mathematical	—	DFunLike.coe CategoryTheory.ConcreteCategory.hom FinBddDistLat instCategory BoundedLatticeHom DistLat.carrier BddDistLat.toDistLat toBddDistLat DistribLattice.toLattice instDistribLatticeCarrier instBoundedOrderCarrier BoundedLatticeHom.instFunLike instConcreteCategoryBoundedLatticeHomCarrier 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 FinBddDistLat instCategory BoundedLatticeHom DistLat.carrier BddDistLat.toDistLat toBddDistLat DistribLattice.toLattice instDistribLatticeCarrier instBoundedOrderCarrier BoundedLatticeHom.instFunLike instConcreteCategoryBoundedLatticeHomCarrier CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
inv_hom_apply 📖	mathematical	—	DFunLike.coe CategoryTheory.ConcreteCategory.hom FinBddDistLat instCategory BoundedLatticeHom DistLat.carrier BddDistLat.toDistLat toBddDistLat DistribLattice.toLattice instDistribLatticeCarrier instBoundedOrderCarrier BoundedLatticeHom.instFunLike instConcreteCategoryBoundedLatticeHomCarrier CategoryTheory.Iso.inv CategoryTheory.Iso.hom	—	CategoryTheory.Iso.hom_inv_id_apply
ofHom_apply 📖	mathematical	—	DFunLike.coe of CategoryTheory.ConcreteCategory.hom FinBddDistLat instCategory BoundedLatticeHom DistLat.carrier BddDistLat.toDistLat toBddDistLat DistribLattice.toLattice instDistribLatticeCarrier instBoundedOrderCarrier BoundedLatticeHom.instFunLike instConcreteCategoryBoundedLatticeHomCarrier ofHom	—	—
ofHom_comp 📖	mathematical	—	ofHom BoundedLatticeHom.comp DistribLattice.toLattice CategoryTheory.CategoryStruct.comp FinBddDistLat CategoryTheory.Category.toCategoryStruct instCategory of	—	—
ofHom_hom 📖	mathematical	—	ofHom DistLat.carrier BddDistLat.toDistLat toBddDistLat instDistribLatticeCarrier instBoundedOrderCarrier isFintype Hom.hom	—	—
ofHom_id 📖	mathematical	—	ofHom BoundedLatticeHom.id DistribLattice.toLattice CategoryTheory.CategoryStruct.id FinBddDistLat CategoryTheory.Category.toCategoryStruct instCategory of	—	—

FinBddDistLat.Hom

Definitions

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

Theorems

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

FinBddDistLat.Hom.Simps

Definitions

Name	Category	Theorems
hom 📖	CompOp	—

FinBddDistLat.Iso

Definitions

Name	Category	Theorems
mk 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mk_hom 📖	mathematical	—	CategoryTheory.Iso.hom FinBddDistLat FinBddDistLat.instCategory FinBddDistLat.ofHom DistLat.carrier DistLat.str BddDistLat.isBoundedOrder FinBddDistLat.isFintype	—	—
mk_inv 📖	mathematical	—	CategoryTheory.Iso.inv FinBddDistLat FinBddDistLat.instCategory FinBddDistLat.ofHom DistLat.carrier DistLat.str BddDistLat.isBoundedOrder FinBddDistLat.isFintype	—	—

(root)

Definitions

Name	Category	Theorems
FinBddDistLat 📖	CompData	20 math math: FinBddDistLat.ofHom_comp, FinBddDistLat.ofHom_apply, FinBddDistLat.dualEquiv_functor, FinBddDistLat.hom_inv_apply, FinBddDistLat.ext_iff, FinBddDistLat.coe_id, FinBddDistLat.inv_hom_apply, finBddDistLat_dual_comp_forget_to_bddDistLat, FinBddDistLat.forget_map, FinBddDistLat.comp_apply, finBoolAlg_dual_comp_forget_to_finBddDistLat, FinBddDistLat.hom_comp, FinBddDistLat.coe_comp, FinBddDistLat.Iso.mk_inv, FinBddDistLat.id_apply, FinBddDistLat.hom_id, FinBddDistLat.dual_map, FinBddDistLat.dualEquiv_inverse, FinBddDistLat.ofHom_id, FinBddDistLat.Iso.mk_hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finBddDistLat_dual_comp_forget_to_bddDistLat 📖	mathematical	—	CategoryTheory.Functor.comp FinBddDistLat FinBddDistLat.instCategory BddDistLat BddDistLat.instCategory FinBddDistLat.dual CategoryTheory.forget₂ BoundedLatticeHom DistLat.carrier BddDistLat.toDistLat FinBddDistLat.toBddDistLat DistribLattice.toLattice FinBddDistLat.instDistribLatticeCarrier FinBddDistLat.instBoundedOrderCarrier BoundedLatticeHom.instFunLike FinBddDistLat.instConcreteCategoryBoundedLatticeHomCarrier BddDistLat.instDistribLatticeCarrier BddDistLat.isBoundedOrder BddDistLat.instConcreteCategoryBoundedLatticeHomCarrier FinBddDistLat.hasForgetToBddDistLat BddDistLat.dual	—	—

---

← Back to Index