Enumerate

📁 Source: Mathlib/Data/Set/Enumerate.lean

Statistics

Metric	Count
Definitions enumerate	1
Theorems enumerate_eq_none, enumerate_eq_none_of_sel, enumerate_inj, enumerate_mem	4
Total	5

Set

Definitions

Name	Category	Theorems
enumerate 📖	CompOp	2 math math: enumerate_eq_none_of_sel, enumerate_eq_none

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
enumerate_eq_none 📖	mathematical	enumerate	enumerate	—	enumerate_eq_none_of_sel
enumerate_eq_none_of_sel 📖	mathematical	—	enumerate	—	—
enumerate_inj 📖	—	Set instMembership enumerate	—	—	zero_add enumerate_mem LT.lt.le
enumerate_mem 📖	mathematical	Set instMembership enumerate	Set instMembership	—	enumerate_eq_none_of_sel instIsEmptyFalse

---

← Back to Index