Multiset

📁 Source: Mathlib/Logic/Equiv/Multiset.lean

Statistics

Metric	Count
Definitions lower, multiset, raise, encodable, decodeMultiset, encodeMultiset	6
Theorems isChain_cons_raise, isChain_raise, lower_raise, raise_chain, raise_lower, raise_sorted	6
Total	12

Denumerable

Definitions

Name	Category	Theorems
lower 📖	CompOp	2 math math: lower_raise, raise_lower
multiset 📖	CompOp	—
raise 📖	CompOp	6 math math: raise_chain, isChain_raise, lower_raise, isChain_cons_raise, raise_lower, raise_sorted

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isChain_cons_raise 📖	mathematical	—	raise	—	isChain_raise
isChain_raise 📖	mathematical	—	raise	—	—
lower_raise 📖	mathematical	—	lower raise	—	raise.eq_2 lower.eq_2
raise_chain 📖	mathematical	—	raise	—	isChain_cons_raise
raise_lower 📖	mathematical	List.SortedLE Nat.instPreorder	raise lower	—	List.SortedLE.pairwise List.Pairwise.sortedLE
raise_sorted 📖	mathematical	—	List.SortedLE Nat.instPreorder raise	—	List.IsChain.sortedLE isChain_raise

Multiset

Definitions

Name	Category	Theorems
encodable 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
decodeMultiset 📖	CompOp	—
encodeMultiset 📖	CompOp	—

---

← Back to Index