BddDistLat

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

Statistics

Metric	Count
Definitions BddDistLat, hom, hom, hom', mk, dual, dualEquiv, hasForgetToBddLat, hasForgetToDistLat, instCategory, instCoeSortType, instConcreteCategoryBoundedLatticeHomCarrier, instDistribLatticeCarrier, instInhabited, isBoundedOrder, of, ofHom, toBddLat, toDistLat	19
Theorems ext, ext_iff, mk_hom, mk_inv, coe_comp, coe_id, coe_of, coe_toBddLat, comp_apply, dualEquiv_functor, dualEquiv_inverse, dual_map, ext, ext_iff, forget_bddLat_lat_eq_forget_distLat_lat, 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, bddDistLat_dual_comp_forget_to_distLat	29
Total	48

BddDistLat

Definitions

Name	Category	Theorems
dual 📖	CompOp	6 math math: dualEquiv_inverse, finBddDistLat_dual_comp_forget_to_bddDistLat, dual_map, dualEquiv_functor, boolAlg_dual_comp_forget_to_bddDistLat, bddDistLat_dual_comp_forget_to_distLat
dualEquiv 📖	CompOp	2 math math: dualEquiv_inverse, dualEquiv_functor
hasForgetToBddLat 📖	CompOp	1 math math: forget_bddLat_lat_eq_forget_distLat_lat
hasForgetToDistLat 📖	CompOp	2 math math: forget_bddLat_lat_eq_forget_distLat_lat, bddDistLat_dual_comp_forget_to_distLat
instCategory 📖	CompOp	26 math math: dualEquiv_inverse, HeytAlg.hasForgetToLat_forget₂_map, hom_id, coe_id, HeytAlg.hasForgetToLat_forget₂_obj_str, ofHom_id, HeytAlg.hasForgetToLat_forget₂_obj_carrier, finBddDistLat_dual_comp_forget_to_bddDistLat, coe_comp, forget_map, dual_map, dualEquiv_functor, inv_hom_apply, Iso.mk_hom, ofHom_apply, HeytAlg.hasForgetToLat_forget₂_obj_isBoundedOrder, id_apply, forget_bddLat_lat_eq_forget_distLat_lat, ofHom_comp, ext_iff, boolAlg_dual_comp_forget_to_bddDistLat, comp_apply, hom_comp, bddDistLat_dual_comp_forget_to_distLat, Iso.mk_inv, hom_inv_apply
instCoeSortType 📖	CompOp	—
instConcreteCategoryBoundedLatticeHomCarrier 📖	CompOp	17 math math: HeytAlg.hasForgetToLat_forget₂_map, coe_id, HeytAlg.hasForgetToLat_forget₂_obj_str, HeytAlg.hasForgetToLat_forget₂_obj_carrier, finBddDistLat_dual_comp_forget_to_bddDistLat, coe_comp, forget_map, inv_hom_apply, ofHom_apply, HeytAlg.hasForgetToLat_forget₂_obj_isBoundedOrder, id_apply, forget_bddLat_lat_eq_forget_distLat_lat, ext_iff, boolAlg_dual_comp_forget_to_bddDistLat, comp_apply, bddDistLat_dual_comp_forget_to_distLat, hom_inv_apply
instDistribLatticeCarrier 📖	CompOp	21 math math: HeytAlg.hasForgetToLat_forget₂_map, ofHom_hom, hom_id, coe_id, HeytAlg.hasForgetToLat_forget₂_obj_str, HeytAlg.hasForgetToLat_forget₂_obj_carrier, finBddDistLat_dual_comp_forget_to_bddDistLat, coe_comp, forget_map, dual_map, inv_hom_apply, ofHom_apply, HeytAlg.hasForgetToLat_forget₂_obj_isBoundedOrder, id_apply, forget_bddLat_lat_eq_forget_distLat_lat, ext_iff, boolAlg_dual_comp_forget_to_bddDistLat, comp_apply, hom_comp, bddDistLat_dual_comp_forget_to_distLat, hom_inv_apply
instInhabited 📖	CompOp	—
isBoundedOrder 📖	CompOp	25 math math: HeytAlg.hasForgetToLat_forget₂_map, ofHom_hom, hom_id, coe_id, HeytAlg.hasForgetToLat_forget₂_obj_str, HeytAlg.hasForgetToLat_forget₂_obj_carrier, finBddDistLat_dual_comp_forget_to_bddDistLat, coe_comp, forget_map, dual_map, inv_hom_apply, Iso.mk_hom, ofHom_apply, HeytAlg.hasForgetToLat_forget₂_obj_isBoundedOrder, id_apply, forget_bddLat_lat_eq_forget_distLat_lat, FinBddDistLat.Iso.mk_inv, ext_iff, boolAlg_dual_comp_forget_to_bddDistLat, comp_apply, hom_comp, bddDistLat_dual_comp_forget_to_distLat, Iso.mk_inv, FinBddDistLat.Iso.mk_hom, hom_inv_apply
of 📖	CompOp	5 math math: ofHom_id, hom_ofHom, ofHom_apply, ofHom_comp, coe_of
ofHom 📖	CompOp	9 math math: HeytAlg.hasForgetToLat_forget₂_map, ofHom_hom, ofHom_id, hom_ofHom, dual_map, Iso.mk_hom, ofHom_apply, ofHom_comp, Iso.mk_inv
toBddLat 📖	CompOp	1 math math: coe_toBddLat
toDistLat 📖	CompOp	38 math math: HeytAlg.hasForgetToLat_forget₂_map, ofHom_hom, FinBddDistLat.ofHom_apply, hom_id, coe_id, HeytAlg.hasForgetToLat_forget₂_obj_str, FinBddDistLat.hom_inv_apply, HeytAlg.hasForgetToLat_forget₂_obj_carrier, FinBddDistLat.ext_iff, BoolAlg.coe_toBddDistLat, FinBddDistLat.coe_id, FinBddDistLat.inv_hom_apply, finBddDistLat_dual_comp_forget_to_bddDistLat, FinBddDistLat.forget_map, coe_comp, coe_toBddLat, forget_map, FinBddDistLat.comp_apply, dual_map, inv_hom_apply, ofHom_apply, HeytAlg.hasForgetToLat_forget₂_obj_isBoundedOrder, FinBddDistLat.ofHom_hom, id_apply, forget_bddLat_lat_eq_forget_distLat_lat, finBoolAlg_dual_comp_forget_to_finBddDistLat, FinBddDistLat.hom_comp, FinBddDistLat.coe_comp, coe_of, ext_iff, boolAlg_dual_comp_forget_to_bddDistLat, FinBddDistLat.id_apply, comp_apply, hom_comp, bddDistLat_dual_comp_forget_to_distLat, FinBddDistLat.hom_id, FinBddDistLat.dual_map, hom_inv_apply

Theorems

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

BddDistLat.Hom

Definitions

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

Theorems

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

BddDistLat.Hom.Simps

Definitions

Name	Category	Theorems
hom 📖	CompOp	—

BddDistLat.Iso

Definitions

Name	Category	Theorems
mk 📖	CompOp	—

Theorems

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

(root)

Definitions

Name	Category	Theorems
BddDistLat 📖	CompData	26 math math: BddDistLat.dualEquiv_inverse, HeytAlg.hasForgetToLat_forget₂_map, BddDistLat.hom_id, BddDistLat.coe_id, HeytAlg.hasForgetToLat_forget₂_obj_str, BddDistLat.ofHom_id, HeytAlg.hasForgetToLat_forget₂_obj_carrier, finBddDistLat_dual_comp_forget_to_bddDistLat, BddDistLat.coe_comp, BddDistLat.forget_map, BddDistLat.dual_map, BddDistLat.dualEquiv_functor, BddDistLat.inv_hom_apply, BddDistLat.Iso.mk_hom, BddDistLat.ofHom_apply, HeytAlg.hasForgetToLat_forget₂_obj_isBoundedOrder, BddDistLat.id_apply, BddDistLat.forget_bddLat_lat_eq_forget_distLat_lat, BddDistLat.ofHom_comp, BddDistLat.ext_iff, boolAlg_dual_comp_forget_to_bddDistLat, BddDistLat.comp_apply, BddDistLat.hom_comp, bddDistLat_dual_comp_forget_to_distLat, BddDistLat.Iso.mk_inv, BddDistLat.hom_inv_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bddDistLat_dual_comp_forget_to_distLat 📖	mathematical	—	CategoryTheory.Functor.comp BddDistLat BddDistLat.instCategory DistLat DistLat.instCategory BddDistLat.dual CategoryTheory.forget₂ BoundedLatticeHom DistLat.carrier BddDistLat.toDistLat DistribLattice.toLattice BddDistLat.instDistribLatticeCarrier BddDistLat.isBoundedOrder BoundedLatticeHom.instFunLike BddDistLat.instConcreteCategoryBoundedLatticeHomCarrier LatticeHom DistLat.str LatticeHom.instFunLike DistLat.instConcreteCategoryLatticeHomCarrier BddDistLat.hasForgetToDistLat DistLat.dual	—	—

---

← Back to Index