Order

📁 Source: Mathlib/Data/Finset/Order.lean

Statistics

Metric	Count
Definitions	0
Theorems finset_le, exists_le	2
Total	2

Directed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finset_le 📖	—	Directed	—	—	Multiset.induction_on instIsEmptyFalse Multiset.mem_cons trans

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_le 📖	mathematical	—	Preorder.toLE	—	Directed.finset_le instIsTransLe directed_id

---

← Back to Index