NonemptyFinLinOrd

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

Statistics

Metric	Count
Definitions hom_succ, NonemptyFinLinOrd, mk, dual, dualEquiv, fintype, hasForgetToFinPartOrd, hasForgetToLinOrd, instBoundedOrderCarrier, instCoeSortType, instConcreteCategoryOrderHomCarrier, instInhabited, instLargeCategory, of, ofHom, toLinOrd, nonemptyFinLinOrdDualCompForgetToFinPartOrd	17
Theorems mk_hom, mk_inv, coe_of, comp_apply, dualEquiv_functor, dualEquiv_inverse, dual_map, epi_iff_surjective, hom_comp, hom_ext, hom_ext_iff, hom_hom_comp, hom_hom_id, hom_hom_ofHom, hom_id, hom_ofHom, id_apply, instHasStrongEpiMonoFactorisations, instSplitEpiCategory, mono_iff_injective, nonempty, ofHom_hom, nonemptyFinLinOrd_dual_comp_forget_to_linOrd	23
Total	40

Fin

Definitions

Name	Category	Theorems
hom_succ 📖	CompOp	—

NonemptyFinLinOrd

Definitions

Name	Category	Theorems
dual 📖	CompOp	4 math math: nonemptyFinLinOrd_dual_comp_forget_to_linOrd, dual_map, dualEquiv_inverse, dualEquiv_functor
dualEquiv 📖	CompOp	2 math math: dualEquiv_inverse, dualEquiv_functor
fintype 📖	CompOp	4 math math: Iso.mk_inv, ofHom_hom, dual_map, Iso.mk_hom
hasForgetToFinPartOrd 📖	CompOp	—
hasForgetToLinOrd 📖	CompOp	3 math math: nonemptyFinLinOrd_dual_comp_forget_to_linOrd, SimplexCategory.toCat_obj, SimplexCategory.toCat_map
instBoundedOrderCarrier 📖	CompOp	—
instCoeSortType 📖	CompOp	—
instConcreteCategoryOrderHomCarrier 📖	CompOp	7 math math: epi_iff_surjective, nonemptyFinLinOrd_dual_comp_forget_to_linOrd, id_apply, comp_apply, SimplexCategory.toCat_obj, SimplexCategory.toCat_map, mono_iff_injective
instInhabited 📖	CompOp	—
instLargeCategory 📖	CompOp	26 math math: instSplitEpiCategory, SimplexCategory.SkeletalFunctor.instEssSurjNonemptyFinLinOrdSkeletalFunctor, epi_iff_surjective, hom_comp, SimplexCategory.isSkeletonOf, Iso.mk_inv, nonemptyFinLinOrd_dual_comp_forget_to_linOrd, SimplexCategory.SkeletalFunctor.isEquivalence, hom_hom_id, dual_map, id_apply, instHasStrongEpiMonoFactorisations, comp_apply, dualEquiv_inverse, hom_hom_comp, SimplexCategory.toCat_obj, dualEquiv_functor, SimplexCategory.skeletalFunctor_obj, SimplexCategory.SkeletalFunctor.instFaithfulNonemptyFinLinOrdSkeletalFunctor, SimplexCategory.skeletalFunctor_map, SimplexCategory.skeletalFunctor.coe_map, SimplexCategory.toCat_map, mono_iff_injective, SimplexCategory.SkeletalFunctor.instFullNonemptyFinLinOrdSkeletalFunctor, Iso.mk_hom, hom_id
of 📖	CompOp	6 math math: coe_of, hom_hom_ofHom, SimplexCategory.toCat_obj, SimplexCategory.skeletalFunctor_obj, SimplexCategory.toCat_map, hom_ofHom
ofHom 📖	CompOp	8 math math: hom_hom_ofHom, Iso.mk_inv, ofHom_hom, dual_map, SimplexCategory.skeletalFunctor_map, SimplexCategory.toCat_map, Iso.mk_hom, hom_ofHom
toLinOrd 📖	CompOp	21 math math: coe_of, epi_iff_surjective, hom_hom_ofHom, hom_comp, Iso.mk_inv, nonemptyFinLinOrd_dual_comp_forget_to_linOrd, hom_ext_iff, ofHom_hom, hom_hom_id, dual_map, nonempty, id_apply, comp_apply, hom_hom_comp, SimplexCategory.toCat_obj, SimplexCategory.skeletalFunctor.coe_map, SimplexCategory.toCat_map, mono_iff_injective, Iso.mk_hom, hom_id, hom_ofHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_of 📖	mathematical	—	LinOrd.carrier toLinOrd of	—	—
comp_apply 📖	mathematical	—	DFunLike.coe CategoryTheory.ConcreteCategory.hom NonemptyFinLinOrd instLargeCategory OrderHom LinOrd.carrier toLinOrd PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinOrd.str OrderHom.instFunLike instConcreteCategoryOrderHomCarrier CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.comp_apply
dualEquiv_functor 📖	mathematical	—	CategoryTheory.Equivalence.functor NonemptyFinLinOrd instLargeCategory dualEquiv dual	—	—
dualEquiv_inverse 📖	mathematical	—	CategoryTheory.Equivalence.inverse NonemptyFinLinOrd instLargeCategory dualEquiv dual	—	—
dual_map 📖	mathematical	—	CategoryTheory.Functor.map NonemptyFinLinOrd instLargeCategory dual ofHom OrderDual LinOrd.carrier toLinOrd OrderDual.instLinearOrder LinOrd.str OrderDual.fintype fintype DFunLike.coe Equiv OrderHom PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder OrderDual.instPreorder EquivLike.toFunLike Equiv.instEquivLike OrderHom.dual LinOrd.Hom.hom CategoryTheory.InducedCategory.Hom.hom LinOrd LinOrd.instCategory	—	—
epi_iff_surjective 📖	mathematical	—	CategoryTheory.Epi NonemptyFinLinOrd instLargeCategory DFunLike.coe CategoryTheory.ConcreteCategory.hom OrderHom LinOrd.carrier toLinOrd PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinOrd.str OrderHom.instFunLike instConcreteCategoryOrderHomCarrier	—	Mathlib.Tactic.Push.not_forall_eq ULift.instNonempty_mathlib nonempty lt_of_le_of_lt le_refl LE.le.trans CategoryTheory.cancel_epi hom_ext OrderHom.ext le_of_lt eq_of_le_of_not_lt CategoryTheory.ConcreteCategory.hom_ofHom CategoryTheory.ConcreteCategory.epi_of_surjective
hom_comp 📖	mathematical	—	LinOrd.Hom.hom toLinOrd CategoryTheory.InducedCategory.Hom.hom NonemptyFinLinOrd LinOrd LinOrd.instCategory CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct instLargeCategory OrderHom.comp LinOrd.carrier PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinOrd.str	—	hom_hom_comp
hom_ext 📖	—	LinOrd.Hom.hom toLinOrd CategoryTheory.InducedCategory.Hom.hom NonemptyFinLinOrd LinOrd LinOrd.instCategory	—	—	CategoryTheory.InducedCategory.hom_ext CategoryTheory.ConcreteCategory.ext
hom_ext_iff 📖	mathematical	—	LinOrd.Hom.hom toLinOrd CategoryTheory.InducedCategory.Hom.hom NonemptyFinLinOrd LinOrd LinOrd.instCategory	—	hom_ext
hom_hom_comp 📖	mathematical	—	LinOrd.Hom.hom toLinOrd CategoryTheory.InducedCategory.Hom.hom NonemptyFinLinOrd LinOrd LinOrd.instCategory CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct instLargeCategory OrderHom.comp LinOrd.carrier PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinOrd.str	—	—
hom_hom_id 📖	mathematical	—	LinOrd.Hom.hom toLinOrd CategoryTheory.InducedCategory.Hom.hom NonemptyFinLinOrd LinOrd LinOrd.instCategory CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct instLargeCategory OrderHom.id LinOrd.carrier PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinOrd.str	—	—
hom_hom_ofHom 📖	mathematical	—	LinOrd.Hom.hom toLinOrd of CategoryTheory.InducedCategory.Hom.hom NonemptyFinLinOrd LinOrd LinOrd.instCategory ofHom	—	—
hom_id 📖	mathematical	—	LinOrd.Hom.hom toLinOrd CategoryTheory.InducedCategory.Hom.hom NonemptyFinLinOrd LinOrd LinOrd.instCategory CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct instLargeCategory OrderHom.id LinOrd.carrier PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinOrd.str	—	hom_hom_id
hom_ofHom 📖	mathematical	—	LinOrd.Hom.hom toLinOrd of CategoryTheory.InducedCategory.Hom.hom NonemptyFinLinOrd LinOrd LinOrd.instCategory ofHom	—	hom_hom_ofHom
id_apply 📖	mathematical	—	DFunLike.coe CategoryTheory.ConcreteCategory.hom NonemptyFinLinOrd instLargeCategory OrderHom LinOrd.carrier toLinOrd PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinOrd.str OrderHom.instFunLike instConcreteCategoryOrderHomCarrier CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.id_apply
instHasStrongEpiMonoFactorisations 📖	mathematical	—	CategoryTheory.Limits.HasStrongEpiMonoFactorisations NonemptyFinLinOrd instLargeCategory	—	Set.instNonemptyElemImage Set.instNonemptyTop nonempty OrderHom.monotone CategoryTheory.ConcreteCategory.mono_of_injective CategoryTheory.strongEpi_of_epi CategoryTheory.strongEpiCategory_of_regularEpiCategory CategoryTheory.regularEpiCategoryOfSplitEpiCategory instSplitEpiCategory epi_iff_surjective
instSplitEpiCategory 📖	mathematical	—	CategoryTheory.SplitEpiCategory NonemptyFinLinOrd instLargeCategory	—	epi_iff_surjective CategoryTheory.IsSplitEpi.mk' nonempty Mathlib.Tactic.Contrapose.contrapose₁ OrderHom.monotone le_of_lt lt_of_le_of_ne hom_ext OrderHom.ext
mono_iff_injective 📖	mathematical	—	CategoryTheory.Mono NonemptyFinLinOrd instLargeCategory DFunLike.coe CategoryTheory.ConcreteCategory.hom OrderHom LinOrd.carrier toLinOrd PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinOrd.str OrderHom.instFunLike instConcreteCategoryOrderHomCarrier	—	ULift.instNonempty_mathlib nonempty le_refl hom_ext OrderHom.ext CategoryTheory.cancel_mono CategoryTheory.ConcreteCategory.mono_of_injective
nonempty 📖	mathematical	—	LinOrd.carrier toLinOrd	—	—
ofHom_hom 📖	mathematical	—	ofHom LinOrd.carrier toLinOrd nonempty LinOrd.str fintype LinOrd.Hom.hom CategoryTheory.InducedCategory.Hom.hom NonemptyFinLinOrd LinOrd LinOrd.instCategory	—	nonempty

NonemptyFinLinOrd.Iso

Definitions

Name	Category	Theorems
mk 📖	CompOp	—

Theorems

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

(root)

Definitions

Name	Category	Theorems
NonemptyFinLinOrd 📖	CompData	30 math math: NonemptyFinLinOrd.instSplitEpiCategory, SimplexCategory.SkeletalFunctor.instEssSurjNonemptyFinLinOrdSkeletalFunctor, NonemptyFinLinOrd.epi_iff_surjective, NonemptyFinLinOrd.hom_hom_ofHom, NonemptyFinLinOrd.hom_comp, SimplexCategory.isSkeletonOf, NonemptyFinLinOrd.Iso.mk_inv, nonemptyFinLinOrd_dual_comp_forget_to_linOrd, NonemptyFinLinOrd.hom_ext_iff, SimplexCategory.SkeletalFunctor.isEquivalence, NonemptyFinLinOrd.ofHom_hom, NonemptyFinLinOrd.hom_hom_id, NonemptyFinLinOrd.dual_map, NonemptyFinLinOrd.id_apply, NonemptyFinLinOrd.instHasStrongEpiMonoFactorisations, NonemptyFinLinOrd.comp_apply, NonemptyFinLinOrd.dualEquiv_inverse, NonemptyFinLinOrd.hom_hom_comp, SimplexCategory.toCat_obj, NonemptyFinLinOrd.dualEquiv_functor, SimplexCategory.skeletalFunctor_obj, SimplexCategory.SkeletalFunctor.instFaithfulNonemptyFinLinOrdSkeletalFunctor, SimplexCategory.skeletalFunctor_map, SimplexCategory.skeletalFunctor.coe_map, SimplexCategory.toCat_map, NonemptyFinLinOrd.mono_iff_injective, SimplexCategory.SkeletalFunctor.instFullNonemptyFinLinOrdSkeletalFunctor, NonemptyFinLinOrd.Iso.mk_hom, NonemptyFinLinOrd.hom_id, NonemptyFinLinOrd.hom_ofHom
nonemptyFinLinOrdDualCompForgetToFinPartOrd 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
nonemptyFinLinOrd_dual_comp_forget_to_linOrd 📖	mathematical	—	CategoryTheory.Functor.comp NonemptyFinLinOrd NonemptyFinLinOrd.instLargeCategory LinOrd LinOrd.instCategory NonemptyFinLinOrd.dual CategoryTheory.forget₂ OrderHom LinOrd.carrier NonemptyFinLinOrd.toLinOrd PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinOrd.str OrderHom.instFunLike NonemptyFinLinOrd.instConcreteCategoryOrderHomCarrier LinOrd.instConcreteCategoryOrderHomCarrier NonemptyFinLinOrd.hasForgetToLinOrd LinOrd.dual	—	—

---

← Back to Index