Option

📁 Source: Mathlib/Data/FinEnum/Option.lean

Statistics

Metric	Count
Definitions insertNone, instFinEnumOptionLast, recEmptyOption, recOnEmptyOption	4
Theorems recEmptyOption_of_card_eq_zero, recEmptyOption_of_card_pos	2
Total	6

FinEnum

Definitions

Name	Category	Theorems
insertNone 📖	CompOp	1 math math: recEmptyOption_of_card_pos
instFinEnumOptionLast 📖	CompOp	—
recEmptyOption 📖	CompOp	2 math math: recEmptyOption_of_card_pos, recEmptyOption_of_card_eq_zero
recOnEmptyOption 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
recEmptyOption_of_card_eq_zero 📖	mathematical	card	recEmptyOption card_eq_zero PEmpty.instIsEmpty	—	card_eq_zero PEmpty.instIsEmpty recEmptyOption.eq_def Unique.instSubsingleton
recEmptyOption_of_card_pos 📖	mathematical	card	recEmptyOption insertNone ULift.instFinEnum fin card_fin	—	card_fin recEmptyOption.eq_def

---

← Back to Index