Finset

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

Statistics

Metric	Count
Definitions	0
Theorems add_sup, add_sup', add_sup'', fold_max_add, inf'_pow, mul_sup', nsmul_inf', nsmul_sup', sup'_add, sup'_add', sup'_mul, sup'_pow, sup_add, sup_add_sup, toFinset_card_eq_one_iff, toFinset_eq_singleton_iff, toFinset_nsmul	17
Total	17

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_sup 📖	mathematical	Nonempty	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup sup Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	sup'_eq_sup add_sup''
add_sup' 📖	mathematical	Nonempty	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid sup' Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	map_finset_sup' LatticeHomClass.toSupHomClass OrderHomClass.toLatticeHomClass RelIso.instRelHomClass
add_sup'' 📖	mathematical	Nonempty	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup sup' Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	add_comm sup'_congr sup'_add'
fold_max_add 📖	mathematical	—	fold WithBot SemilatticeSup.toMax Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder WithBot.linearOrder instCommutativeMax instAssociativeMax Bot.bot WithBot.bot WithBot.add WithBot.some WithBot.semilatticeSup	—	induction_on instCommutativeMax instAssociativeMax fold_congr fold_insert max_add_add_right WithBot.addRightMono
inf'_pow 📖	mathematical	Nonempty	Monoid.toNatPow inf' Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	map_finset_inf' LatticeHomClass.toInfHomClass OrderHomClass.toLatticeHomClass OrderHom.instOrderHomClass pow_left_mono
mul_sup' 📖	mathematical	Nonempty	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid sup' Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	map_finset_sup' LatticeHomClass.toSupHomClass OrderHomClass.toLatticeHomClass RelIso.instRelHomClass
nsmul_inf' 📖	mathematical	Nonempty	AddMonoid.toNatSMul inf' Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	map_finset_inf' LatticeHomClass.toInfHomClass OrderHomClass.toLatticeHomClass OrderHom.instOrderHomClass nsmul_right_mono
nsmul_sup' 📖	mathematical	Nonempty	AddMonoid.toNatSMul sup' Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	map_finset_sup' LatticeHomClass.toSupHomClass OrderHomClass.toLatticeHomClass OrderHom.instOrderHomClass nsmul_right_mono
sup'_add 📖	mathematical	Nonempty	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid sup' Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	map_finset_sup' LatticeHomClass.toSupHomClass OrderHomClass.toLatticeHomClass RelIso.instRelHomClass
sup'_add' 📖	mathematical	Nonempty	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup sup' Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	le_antisymm add_le_of_le_tsub_right_of_le CanonicallyOrderedAdd.toExistsAddOfLE CanonicallyOrderedAdd.toAddLeftMono le_sup'_of_le le_add_self sup'_le le_tsub_of_add_le_right le_sup' le_imp_le_of_le_of_le le_refl add_le_add_left covariant_swap_add_of_covariant_add
sup'_mul 📖	mathematical	Nonempty	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid sup' Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	map_finset_sup' LatticeHomClass.toSupHomClass OrderHomClass.toLatticeHomClass RelIso.instRelHomClass
sup'_pow 📖	mathematical	Nonempty	Monoid.toNatPow sup' Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	map_finset_sup' LatticeHomClass.toSupHomClass OrderHomClass.toLatticeHomClass OrderHom.instOrderHomClass pow_left_mono
sup_add 📖	mathematical	Nonempty	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup sup Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	sup'_eq_sup sup'_add'
sup_add_sup 📖	mathematical	Nonempty	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup sup Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder SProd.sprod Finset instSProd	—	sup_add add_sup sup_product_left

Multiset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toFinset_card_eq_one_iff 📖	mathematical	—	Finset.card toFinset Multiset AddMonoid.toNatSMul AddCommMonoid.toAddMonoid AddCancelCommMonoid.toAddCommMonoid instAddCancelCommMonoid card instSingleton	—	—
toFinset_eq_singleton_iff 📖	mathematical	—	toFinset Finset Finset.instSingleton Multiset AddMonoid.toNatSMul AddCommMonoid.toAddMonoid AddCancelCommMonoid.toAddCommMonoid instAddCancelCommMonoid card instSingleton	—	Finset.empty_ne_singleton toFinset_zero card_eq_zero ext' count_nsmul count_singleton count.congr_simp mul_one Finset.mem_singleton mem_toFinset count_eq_zero_of_notMem toFinset_nsmul toFinset_singleton
toFinset_nsmul 📖	mathematical	—	toFinset Multiset AddMonoid.toNatSMul AddCommMonoid.toAddMonoid AddCancelCommMonoid.toAddCommMonoid instAddCancelCommMonoid	—	zero_add one_nsmul add_nsmul toFinset_add Finset.union_idempotent

---

← Back to Index