Bounds

📁 Source: Mathlib/Data/Nat/Choose/Bounds.lean

Statistics

Metric	Count
Definitions	0
Theorems choose_le_descFactorial, choose_le_pow, choose_le_pow_div, choose_le_two_pow, choose_lt_descFactorial, choose_lt_pow, choose_lt_pow_div, choose_lt_two_pow, choose_succ_le_two_pow, pow_le_choose	10
Total	10

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
choose_le_descFactorial 📖	mathematical	—	choose descFactorial	—	choose_eq_descFactorial_div_factorial
choose_le_pow 📖	mathematical	—	choose Monoid.toNatPow instMonoid	—	LE.le.trans choose_le_descFactorial descFactorial_le_pow
choose_le_pow_div 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring choose DivInvMonoid.toDiv GroupWithZero.toDivInvMonoid DivisionSemiring.toGroupWithZero Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero factorial	—	le_div_iff₀' PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono cast_zero IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing IsStrictOrderedRing.toZeroLEOneClass IsStrictOrderedRing.toCharZero factorial_pos descFactorial_eq_factorial_mul_choose descFactorial_le_pow
choose_le_two_pow 📖	mathematical	—	choose Monoid.toNatPow instMonoid	—	choose_self pow_zero instZeroLEOneClass LT.lt.le choose_lt_two_pow
choose_lt_descFactorial 📖	mathematical	—	choose descFactorial	—	choose_eq_descFactorial_div_factorial
choose_lt_pow 📖	mathematical	—	choose Monoid.toNatPow instMonoid	—	LE.le.trans_lt choose_le_descFactorial descFactorial_lt_pow
choose_lt_pow_div 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring choose DivInvMonoid.toDiv GroupWithZero.toDivInvMonoid DivisionSemiring.toGroupWithZero Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero factorial	—	lt_div_iff₀' PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono cast_zero IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing IsStrictOrderedRing.toZeroLEOneClass IsStrictOrderedRing.toCharZero factorial_pos descFactorial_eq_factorial_mul_choose descFactorial_lt_pow
choose_lt_two_pow 📖	mathematical	—	choose Monoid.toNatPow instMonoid	—	lt_of_le_of_lt choose_succ_le_two_pow
choose_succ_le_two_pow 📖	mathematical	—	choose Monoid.toNatPow instMonoid	—	—
pow_le_choose 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder DivInvMonoid.toDiv GroupWithZero.toDivInvMonoid DivisionSemiring.toGroupWithZero Semifield.toDivisionSemiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring factorial choose	—	div_le_iff₀' PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono cast_zero IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing IsStrictOrderedRing.toZeroLEOneClass IsStrictOrderedRing.toCharZero factorial_pos descFactorial_eq_factorial_mul_choose pow_sub_le_descFactorial

---

← Back to Index