Finset

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

Statistics

Metric	Count
Definitions	0
Theorems mul_sup₀, sup_mul₀, cast_finsetInf', cast_finsetSup, cast_finsetSup'	5
Total	5

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mul_sup₀ 📖	mathematical	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib sup Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	induction sup_empty bot_eq_zero' MulZeroClass.mul_zero sup_insert mul_max CanonicallyOrderedAdd.toMulLeftMono
sup_mul₀ 📖	mathematical	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib sup Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	induction sup_empty bot_eq_zero' MulZeroClass.zero_mul sup_insert max_mul CanonicallyOrderedAdd.toMulRightMono

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cast_finsetInf' 📖	mathematical	Finset.Nonempty	AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring Finset.inf' Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeNat instDistribLatticeOfLinearOrder	—	Finset.comp_inf'_eq_inf'_comp cast_min
cast_finsetSup 📖	mathematical	—	AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring Finset.sup Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeNat instOrderBot instDistribLatticeOfLinearOrder	—	Finset.comp_sup_eq_sup_comp cast_max cast_zero bot_eq_zero'
cast_finsetSup' 📖	mathematical	Finset.Nonempty	AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring Finset.sup' Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeNat instDistribLatticeOfLinearOrder	—	Finset.comp_sup'_eq_sup'_comp cast_max

---

← Back to Index