Order

📁 Source: Mathlib/Data/DFinsupp/Order.lean

Statistics

Metric	Count
Definitions decidableLE, instLE, instOrderBot, instPartialOrder, instPreorder, instSemilatticeInf, instSemilatticeSup, lattice, orderEmbeddingToFun, tsub	10
Theorems add_eq_zero_iff, bot_eq_zero, coe_inf, coe_le_coe, coe_lt_coe, coe_mono, coe_orderEmbeddingToFun, coe_strictMono, coe_sup, coe_tsub, disjoint_iff, inf_apply, instAddLeftReflectLE, instCanonicallyOrderedAddOfAddLeftMono, instIsOrderedAddMonoid, instIsOrderedCancelAddMonoid, instOrderedSub, instPosSMulMono, instPosSMulReflectLE, instPosSMulStrictMono, instSMulPosMono, instSMulPosReflectLE, instSMulPosReflectLT, instSMulPosStrictMono, le_def, le_iff, le_iff', lt_def, orderEmbeddingToFun_apply, single_le_iff, single_tsub, subset_support_tsub, sup_apply, support_inf, support_inf_union_support_sup, support_mono, support_monotone, support_sup, support_sup_union_support_inf, support_tsub, tsub_apply	41
Total	51

DFinsupp

Definitions

Name	Category	Theorems
decidableLE 📖	CompOp	—
instLE 📖	CompOp	14 math math: lt_def, le_iff', single_le_iff, le_def, instCanonicallyOrderedAddOfAddLeftMono, toMultiset_le_toMultiset, le_iff, coe_orderEmbeddingToFun, instAddLeftReflectLE, bot_eq_zero, instOrderedSub, Multiset.toDFinsupp_le_toDFinsupp, coe_le_coe, orderEmbeddingToFun_apply
instOrderBot 📖	CompOp	4 math math: disjoint_iff, card_Iic, bot_eq_zero, card_Iio
instPartialOrder 📖	CompOp	3 math math: instIsOrderedCancelAddMonoid, disjoint_iff, instIsOrderedAddMonoid
instPreorder 📖	CompOp	27 math math: coe_mono, toLex_monotone, Multiset.Icc_eq, lt_def, instSMulPosMono, card_Iic, wellFoundedLT', wellFoundedLT, instPosSMulStrictMono, card_Ioo, Icc_eq, instPosSMulReflectLE, instPosSMulMono, instSMulPosReflectLT, coe_strictMono, card_Ico, toColex_monotone, instSMulPosReflectLE, Multiset.toDFinsupp_lt_toDFinsupp, toMultiset_lt_toMultiset, card_Iio, coe_lt_coe, card_Icc, card_Ioc, wellFoundedLT_of_finite, instSMulPosStrictMono, support_monotone
instSemilatticeInf 📖	CompOp	7 math math: support_inf, toMultiset_inf, inf_apply, support_sup_union_support_inf, coe_inf, Multiset.toDFinsupp_inter, support_inf_union_support_sup
instSemilatticeSup 📖	CompOp	7 math math: toMultiset_sup, coe_sup, sup_apply, support_sup_union_support_inf, Multiset.toDFinsupp_union, support_inf_union_support_sup, support_sup
lattice 📖	CompOp	2 math math: Multiset.uIcc_eq, card_uIcc
orderEmbeddingToFun 📖	CompOp	2 math math: coe_orderEmbeddingToFun, orderEmbeddingToFun_apply
tsub 📖	CompOp	6 math math: tsub_apply, coe_tsub, subset_support_tsub, support_tsub, single_tsub, instOrderedSub

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_eq_zero_iff 📖	mathematical	CanonicallyOrderedAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Preorder.toLE PartialOrder.toPreorder	DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAdd instZero	—	Unique.instSubsingleton
bot_eq_zero 📖	mathematical	CanonicallyOrderedAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Preorder.toLE PartialOrder.toPreorder	Bot.bot DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid OrderBot.toBot instLE instOrderBot instZero	—	—
coe_inf 📖	mathematical	—	DFunLike.coe DFinsupp instDFunLike SemilatticeInf.toMin instSemilatticeInf Pi.instMinForall_mathlib	—	—
coe_le_coe 📖	mathematical	—	Pi.hasLe DFunLike.coe DFinsupp instDFunLike instLE	—	—
coe_lt_coe 📖	mathematical	—	Preorder.toLT Pi.preorder DFunLike.coe DFinsupp instDFunLike instPreorder	—	—
coe_mono 📖	mathematical	—	Monotone DFinsupp instPreorder Pi.preorder DFunLike.coe instDFunLike	—	—
coe_orderEmbeddingToFun 📖	mathematical	—	DFunLike.coe OrderEmbedding DFinsupp instLE Pi.hasLe instFunLikeOrderEmbedding orderEmbeddingToFun instDFunLike	—	—
coe_strictMono 📖	mathematical	—	Monotone DFinsupp instPreorder Pi.preorder DFunLike.coe instDFunLike	—	—
coe_sup 📖	mathematical	—	DFunLike.coe DFinsupp instDFunLike SemilatticeSup.toMax instSemilatticeSup Pi.instMaxForall_mathlib	—	—
coe_tsub 📖	mathematical	CanonicallyOrderedAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Preorder.toLE PartialOrder.toPreorder OrderedSub	DFunLike.coe DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instDFunLike tsub Pi.instSub	—	tsub_apply
disjoint_iff 📖	mathematical	CanonicallyOrderedAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Disjoint DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instPartialOrder instOrderBot Finset Finset.partialOrder Finset.instOrderBot support LinearOrder.toDecidableEq	—	disjoint_iff bot_eq_zero support_eq_empty support_inf
inf_apply 📖	mathematical	—	DFunLike.coe DFinsupp instDFunLike SemilatticeInf.toMin instSemilatticeInf	—	zipWith_apply
instAddLeftReflectLE 📖	mathematical	AddLeftReflectLE AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Preorder.toLE PartialOrder.toPreorder	DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAdd instLE	—	le_of_add_le_add_left
instCanonicallyOrderedAddOfAddLeftMono 📖	mathematical	CanonicallyOrderedAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Preorder.toLE PartialOrder.toPreorder OrderedSub AddLeftMono	DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAdd instLE	—	ext add_tsub_cancel_of_le CanonicallyOrderedAdd.toExistsAddOfLE le_add_self le_self_add
instIsOrderedAddMonoid 📖	mathematical	IsOrderedAddMonoid	DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid addCommMonoid instPartialOrder	—	add_le_add_left covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono
instIsOrderedCancelAddMonoid 📖	mathematical	IsOrderedCancelAddMonoid	DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid addCommMonoid instPartialOrder	—	instIsOrderedAddMonoid IsOrderedCancelAddMonoid.toIsOrderedAddMonoid le_of_add_le_add_left IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT IsCancelAdd.toIsLeftCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd IsOrderedCancelAddMonoid.toAddLeftReflectLT
instOrderedSub 📖	mathematical	CanonicallyOrderedAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Preorder.toLE PartialOrder.toPreorder OrderedSub	DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instLE instAdd tsub	—	tsub_le_iff_right
instPosSMulMono 📖	mathematical	PosSMulMono SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	DFinsupp instZero instSMulZeroClass instPreorder	—	PosSMulMono.lift Pi.instPosSMulMono coe_le_coe coe_smul
instPosSMulReflectLE 📖	mathematical	PosSMulReflectLE SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	DFinsupp instZero instSMulZeroClass instPreorder	—	PosSMulReflectLE.lift Pi.instPosSMulReflectLE coe_le_coe coe_smul
instPosSMulStrictMono 📖	mathematical	PosSMulStrictMono SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	DFinsupp instZero instSMulZeroClass instPreorder	—	PosSMulStrictMono.lift Pi.instPosSMulStrictMono coe_le_coe coe_smul
instSMulPosMono 📖	mathematical	SMulPosMono SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	DFinsupp instZero instSMulZeroClass instPreorder	—	SMulPosMono.lift Pi.instSMulPosMono coe_le_coe coe_smul coe_zero
instSMulPosReflectLE 📖	mathematical	SMulPosReflectLE SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	DFinsupp instZero instSMulZeroClass instPreorder	—	SMulPosReflectLE.lift Pi.instSMulPosReflectLE coe_le_coe coe_smul coe_zero
instSMulPosReflectLT 📖	mathematical	SMulPosReflectLT SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction PartialOrder.toPreorder	DFinsupp instZero instSMulZeroClass instPreorder	—	SMulPosReflectLT.lift Pi.instSMulPosReflectLT coe_le_coe coe_smul coe_zero
instSMulPosStrictMono 📖	mathematical	SMulPosStrictMono SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction PartialOrder.toPreorder	DFinsupp instZero instSMulZeroClass instPreorder	—	SMulPosStrictMono.lift Pi.instSMulPosStrictMono coe_le_coe coe_smul coe_zero
le_def 📖	mathematical	—	DFinsupp instLE DFunLike.coe instDFunLike	—	—
le_iff 📖	mathematical	CanonicallyOrderedAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Preorder.toLE PartialOrder.toPreorder	DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instLE DFunLike.coe instDFunLike	—	le_iff' Finset.Subset.refl
le_iff' 📖	mathematical	CanonicallyOrderedAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Preorder.toLE PartialOrder.toPreorder Finset Finset.instHasSubset support AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	DFinsupp instLE DFunLike.coe instDFunLike	—	zero_le notMem_support_iff
lt_def 📖	mathematical	—	DFinsupp Preorder.toLT instPreorder instLE Preorder.toLE DFunLike.coe instDFunLike	—	Pi.lt_def
orderEmbeddingToFun_apply 📖	mathematical	—	DFunLike.coe OrderEmbedding DFinsupp instLE Pi.hasLe instFunLikeOrderEmbedding orderEmbeddingToFun instDFunLike	—	—
single_le_iff 📖	mathematical	CanonicallyOrderedAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Preorder.toLE PartialOrder.toPreorder	DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instLE single DFunLike.coe instDFunLike	—	le_iff' support_single_subset single_apply
single_tsub 📖	mathematical	CanonicallyOrderedAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Preorder.toLE PartialOrder.toPreorder OrderedSub	single AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFinsupp tsub	—	ext eq_or_ne tsub_apply single_eq_same single_eq_of_ne tsub_self
subset_support_tsub 📖	mathematical	CanonicallyOrderedAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Preorder.toLE PartialOrder.toPreorder OrderedSub	Finset Finset.instHasSubset Finset.instSDiff support AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFinsupp tsub	—	coe_tsub tsub_zero
sup_apply 📖	mathematical	—	DFunLike.coe DFinsupp instDFunLike SemilatticeSup.toMax instSemilatticeSup	—	zipWith_apply
support_inf 📖	mathematical	CanonicallyOrderedAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	support AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid LinearOrder.toDecidableEq DFinsupp SemilatticeInf.toMin instSemilatticeInf Finset Finset.instInter	—	Finset.ext inf_apply
support_inf_union_support_sup 📖	mathematical	—	Finset Finset.instUnion support DFinsupp SemilatticeInf.toMin instSemilatticeInf Lattice.toSemilatticeInf SemilatticeSup.toMax instSemilatticeSup Lattice.toSemilatticeSup	—	Finset.coe_injective compl_injective Set.ext Finset.coe_union Set.compl_union
support_mono 📖	mathematical	CanonicallyOrderedAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Preorder.toLE PartialOrder.toPreorder DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instLE	Finset Finset.instHasSubset support	—	support_monotone
support_monotone 📖	mathematical	CanonicallyOrderedAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Preorder.toLE PartialOrder.toPreorder	Monotone DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finset instPreorder Finset.partialOrder support	—	mem_support_iff pos_iff_ne_zero LT.lt.trans_le
support_sup 📖	mathematical	CanonicallyOrderedAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	support AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid LinearOrder.toDecidableEq DFinsupp SemilatticeSup.toMax instSemilatticeSup Lattice.toSemilatticeSup Finset Finset.instUnion	—	Finset.ext sup_apply
support_sup_union_support_inf 📖	mathematical	—	Finset Finset.instUnion support DFinsupp SemilatticeSup.toMax instSemilatticeSup Lattice.toSemilatticeSup SemilatticeInf.toMin instSemilatticeInf Lattice.toSemilatticeInf	—	Finset.union_comm support_inf_union_support_sup
support_tsub 📖	mathematical	CanonicallyOrderedAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Preorder.toLE PartialOrder.toPreorder OrderedSub	Finset Finset.instHasSubset support AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFinsupp tsub	—	coe_tsub
tsub_apply 📖	mathematical	CanonicallyOrderedAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Preorder.toLE PartialOrder.toPreorder OrderedSub	DFunLike.coe DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instDFunLike tsub	—	zipWith_apply

---

← Back to Index