DershowitzManna

📁 Source: Mathlib/Data/Multiset/DershowitzManna.lean

Statistics

Metric	Count
Definitions IsDershowitzMannaLT, instWellFoundedIsDershowitzMannaLT	2
Theorems trans, wellFounded_isDershowitzMannaLT	2
Total	4

Multiset

Definitions

Name	Category	Theorems
IsDershowitzMannaLT 📖	MathDef	1 math math: wellFounded_isDershowitzMannaLT
instWellFoundedIsDershowitzMannaLT 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
wellFounded_isDershowitzMannaLT 📖	mathematical	—	Multiset IsDershowitzMannaLT	—	—

Multiset.IsDershowitzMannaLT

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
trans 📖	—	Multiset.IsDershowitzMannaLT	—	—	Unique.instSubsingleton Multiset.instCanonicallyOrderedAdd add_assoc add_right_comm Multiset.inter_add_sub_of_add_eq_add add_comm AddRightCancelSemigroup.toIsRightCancelAdd Multiset.inter_comm LT.lt.trans Multiset.mem_sub Multiset.count_eq_zero_of_notMem Multiset.count_pos Multiset.mem_of_le Multiset.sub_le_self

---

← Back to Index