LinOrd

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

Statistics

Metric	Count
Definitions LinOrd, hom, hom, hom', mk, dual, dualEquiv, hasForgetToLat, instCategory, instConcreteCategoryOrderHomCarrier, instInhabited, ofHom	12
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, linOrd_dual_comp_forget_to_Lat	27
Total	39

LinOrd

Definitions

Name	Category	Theorems
dual 📖	CompOp	5 math math: dual_map, nonemptyFinLinOrd_dual_comp_forget_to_linOrd, dualEquiv_functor, linOrd_dual_comp_forget_to_Lat, dualEquiv_inverse
dualEquiv 📖	CompOp	2 math math: dualEquiv_functor, dualEquiv_inverse
hasForgetToLat 📖	CompOp	3 math math: SimplexCategory.toCat_obj, linOrd_dual_comp_forget_to_Lat, SimplexCategory.toCat_map
instCategory 📖	CompOp	32 math math: ofHom_apply, hom_id, dual_map, hom_inv_apply, inv_hom_apply, Iso.mk_hom, NonemptyFinLinOrd.hom_hom_ofHom, id_apply, NonemptyFinLinOrd.hom_comp, ofHom_id, nonemptyFinLinOrd_dual_comp_forget_to_linOrd, NonemptyFinLinOrd.hom_ext_iff, NonemptyFinLinOrd.ofHom_hom, forget_map, ext_iff, NonemptyFinLinOrd.hom_hom_id, NonemptyFinLinOrd.dual_map, Iso.mk_inv, ofHom_comp, coe_id, NonemptyFinLinOrd.hom_hom_comp, SimplexCategory.toCat_obj, hom_comp, dualEquiv_functor, SimplexCategory.skeletalFunctor.coe_map, linOrd_dual_comp_forget_to_Lat, SimplexCategory.toCat_map, comp_apply, coe_comp, dualEquiv_inverse, NonemptyFinLinOrd.hom_id, NonemptyFinLinOrd.hom_ofHom
instConcreteCategoryOrderHomCarrier 📖	CompOp	13 math math: ofHom_apply, hom_inv_apply, inv_hom_apply, id_apply, nonemptyFinLinOrd_dual_comp_forget_to_linOrd, forget_map, ext_iff, coe_id, SimplexCategory.toCat_obj, linOrd_dual_comp_forget_to_Lat, SimplexCategory.toCat_map, comp_apply, coe_comp
instInhabited 📖	CompOp	—
ofHom 📖	CompOp	8 math math: ofHom_apply, dual_map, Iso.mk_hom, ofHom_id, Iso.mk_inv, ofHom_comp, ofHom_hom, hom_ofHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_comp 📖	mathematical	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom LinOrd instCategory OrderHom PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder str OrderHom.instFunLike instConcreteCategoryOrderHomCarrier CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	—
coe_id 📖	mathematical	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom LinOrd instCategory OrderHom PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder str OrderHom.instFunLike instConcreteCategoryOrderHomCarrier CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
coe_of 📖	mathematical	—	carrier of	—	—
comp_apply 📖	mathematical	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom LinOrd instCategory OrderHom PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder str OrderHom.instFunLike instConcreteCategoryOrderHomCarrier CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	—
dualEquiv_functor 📖	mathematical	—	CategoryTheory.Equivalence.functor LinOrd instCategory dualEquiv dual	—	—
dualEquiv_inverse 📖	mathematical	—	CategoryTheory.Equivalence.inverse LinOrd instCategory dualEquiv dual	—	—
dual_map 📖	mathematical	—	CategoryTheory.Functor.map LinOrd instCategory dual ofHom OrderDual carrier OrderDual.instLinearOrder str DFunLike.coe Equiv OrderHom PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder OrderDual.instPreorder EquivLike.toFunLike Equiv.instEquivLike OrderHom.dual Hom.hom	—	—
ext 📖	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom LinOrd instCategory OrderHom PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder str OrderHom.instFunLike instConcreteCategoryOrderHomCarrier	—	—	CategoryTheory.ConcreteCategory.hom_ext
ext_iff 📖	mathematical	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom LinOrd instCategory OrderHom PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder str OrderHom.instFunLike instConcreteCategoryOrderHomCarrier	—	ext
forget_map 📖	mathematical	—	CategoryTheory.Functor.map LinOrd instCategory CategoryTheory.types CategoryTheory.forget OrderHom carrier PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder str OrderHom.instFunLike instConcreteCategoryOrderHomCarrier DFunLike.coe CategoryTheory.ConcreteCategory.hom	—	—
hom_comp 📖	mathematical	—	Hom.hom CategoryTheory.CategoryStruct.comp LinOrd CategoryTheory.Category.toCategoryStruct instCategory OrderHom.comp carrier PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder str	—	—
hom_ext 📖	—	Hom.hom	—	—	Hom.ext
hom_ext_iff 📖	mathematical	—	Hom.hom	—	hom_ext
hom_id 📖	mathematical	—	Hom.hom CategoryTheory.CategoryStruct.id LinOrd CategoryTheory.Category.toCategoryStruct instCategory OrderHom.id carrier PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder str	—	—
hom_inv_apply 📖	mathematical	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom LinOrd instCategory OrderHom PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder str OrderHom.instFunLike instConcreteCategoryOrderHomCarrier CategoryTheory.Iso.hom CategoryTheory.Iso.inv	—	CategoryTheory.Iso.inv_hom_id_apply
hom_ofHom 📖	mathematical	—	Hom.hom of ofHom	—	—
id_apply 📖	mathematical	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom LinOrd instCategory OrderHom PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder str OrderHom.instFunLike instConcreteCategoryOrderHomCarrier CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
inv_hom_apply 📖	mathematical	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom LinOrd instCategory OrderHom PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder str OrderHom.instFunLike instConcreteCategoryOrderHomCarrier CategoryTheory.Iso.inv CategoryTheory.Iso.hom	—	CategoryTheory.Iso.hom_inv_id_apply
ofHom_apply 📖	mathematical	—	DFunLike.coe of carrier CategoryTheory.ConcreteCategory.hom LinOrd instCategory OrderHom PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder str OrderHom.instFunLike instConcreteCategoryOrderHomCarrier ofHom	—	—
ofHom_comp 📖	mathematical	—	ofHom OrderHom.comp PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder CategoryTheory.CategoryStruct.comp LinOrd CategoryTheory.Category.toCategoryStruct instCategory of	—	—
ofHom_hom 📖	mathematical	—	ofHom carrier str Hom.hom	—	—
ofHom_id 📖	mathematical	—	ofHom OrderHom.id PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder CategoryTheory.CategoryStruct.id LinOrd CategoryTheory.Category.toCategoryStruct instCategory of	—	—

LinOrd.Hom

Definitions

Name	Category	Theorems
hom 📖	CompOp	16 math math: LinOrd.hom_id, LinOrd.dual_map, NonemptyFinLinOrd.hom_hom_ofHom, NonemptyFinLinOrd.hom_comp, NonemptyFinLinOrd.hom_ext_iff, NonemptyFinLinOrd.ofHom_hom, NonemptyFinLinOrd.hom_hom_id, NonemptyFinLinOrd.dual_map, LinOrd.hom_ext_iff, NonemptyFinLinOrd.hom_hom_comp, LinOrd.hom_comp, LinOrd.ofHom_hom, SimplexCategory.skeletalFunctor.coe_map, NonemptyFinLinOrd.hom_id, NonemptyFinLinOrd.hom_ofHom, LinOrd.hom_ofHom
hom' 📖	CompOp	1 math math: ext_iff

Theorems

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

LinOrd.Hom.Simps

Definitions

Name	Category	Theorems
hom 📖	CompOp	—

LinOrd.Iso

Definitions

Name	Category	Theorems
mk 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mk_hom 📖	mathematical	—	CategoryTheory.Iso.hom LinOrd LinOrd.instCategory LinOrd.ofHom LinOrd.carrier LinOrd.str OrderHomClass.toOrderHom OrderIso Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instFunLikeOrderIso	—	—
mk_inv 📖	mathematical	—	CategoryTheory.Iso.inv LinOrd LinOrd.instCategory LinOrd.ofHom LinOrd.carrier LinOrd.str OrderHomClass.toOrderHom OrderIso Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instFunLikeOrderIso OrderIso.symm	—	—

(root)

Definitions

Name	Category	Theorems
LinOrd 📖	CompData	32 math math: LinOrd.ofHom_apply, LinOrd.hom_id, LinOrd.dual_map, LinOrd.hom_inv_apply, LinOrd.inv_hom_apply, LinOrd.Iso.mk_hom, NonemptyFinLinOrd.hom_hom_ofHom, LinOrd.id_apply, NonemptyFinLinOrd.hom_comp, LinOrd.ofHom_id, nonemptyFinLinOrd_dual_comp_forget_to_linOrd, NonemptyFinLinOrd.hom_ext_iff, NonemptyFinLinOrd.ofHom_hom, LinOrd.forget_map, LinOrd.ext_iff, NonemptyFinLinOrd.hom_hom_id, NonemptyFinLinOrd.dual_map, LinOrd.Iso.mk_inv, LinOrd.ofHom_comp, LinOrd.coe_id, NonemptyFinLinOrd.hom_hom_comp, SimplexCategory.toCat_obj, LinOrd.hom_comp, LinOrd.dualEquiv_functor, SimplexCategory.skeletalFunctor.coe_map, linOrd_dual_comp_forget_to_Lat, SimplexCategory.toCat_map, LinOrd.comp_apply, LinOrd.coe_comp, LinOrd.dualEquiv_inverse, NonemptyFinLinOrd.hom_id, NonemptyFinLinOrd.hom_ofHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
linOrd_dual_comp_forget_to_Lat 📖	mathematical	—	CategoryTheory.Functor.comp LinOrd LinOrd.instCategory Lat Lat.instCategory LinOrd.dual CategoryTheory.forget₂ OrderHom LinOrd.carrier PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinOrd.str OrderHom.instFunLike LinOrd.instConcreteCategoryOrderHomCarrier LatticeHom Lat.carrier Lat.str LatticeHom.instFunLike Lat.instConcreteCategoryLatticeHomCarrier LinOrd.hasForgetToLat Lat.dual	—	—

---

← Back to Index