Finset

📁 Source: Mathlib/Algebra/Order/GroupWithZero/Finset.lean

Statistics

Metric	Count
Definitions	0
Theorems inf'_mul_le_mul_inf'_of_nonneg, mul_inf_le_inf_mul_of_nonneg, mul₀_sup', sup'_div₀, sup'_mul_le_mul_sup'_of_nonneg, sup'_mul₀, sup_div₀, sup_mul_le_mul_sup_of_nonneg	8
Total	8

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inf'_mul_le_mul_inf'_of_nonneg 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Nonempty	MulZeroClass.toMul inf' Pi.instMul	—	le_inf' mul_le_mul inf'_le
mul_inf_le_inf_mul_of_nonneg 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass	MulZeroClass.toMul inf Pi.instMul	—	le_inf mul_le_mul inf_le
mul₀_sup' 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero Nonempty	MulZeroClass.toMul sup'	—	MulZeroClass.zero_mul sup'_congr sup'_const map_finset_sup' OrderIsoClass.toSupHomClass OrderIso.instOrderIsoClass lt_of_le_of_ne
sup'_div₀ 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero Nonempty	DivInvMonoid.toDiv GroupWithZero.toDivInvMonoid sup'	—	div_zero sup'_congr sup'_const map_finset_sup' OrderIsoClass.toSupHomClass OrderIso.instOrderIsoClass lt_of_le_of_ne
sup'_mul_le_mul_sup'_of_nonneg 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Nonempty	sup' Pi.instMul MulZeroClass.toMul	—	sup'_le mul_le_mul le_sup' LE.le.trans
sup'_mul₀ 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero Nonempty	MulZeroClass.toMul sup'	—	MulZeroClass.mul_zero sup'_congr sup'_const map_finset_sup' OrderIsoClass.toSupHomClass OrderIso.instOrderIsoClass lt_of_le_of_ne
sup_div₀ 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero	DivInvMonoid.toDiv GroupWithZero.toDivInvMonoid sup Lattice.toSemilatticeSup LinearOrderedCommMonoidWithZero.toOrderBot	—	eq_empty_or_nonempty sup_empty bot_unique zero_le' zero_div sup'_eq_sup sup'_div₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE LinearOrderedCommMonoidWithZero.toMulPosStrictMono
sup_mul_le_mul_sup_of_nonneg 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass	sup Pi.instMul MulZeroClass.toMul	—	sup_le mul_le_mul le_sup LE.le.trans

---

← Back to Index