FinEnum

Statistics

Metric	Count
Definitions `FinEnum`, `enum`, `finEnum`, `finEnum`, `finEnumPropLeft`, `finEnumPropProp`, `finEnumPropRight`, `enum`, `finEnum`, `card`, `decEq`, `empty`, `equiv`, `fin`, `instFintype`, `instSigma`, `instSubtypeMemListOfDecidableEq`, `instUnique`, `instUniqueOfIsEmpty`, `ofEquiv`, `ofInjective`, `ofIsEmpty`, `ofList`, `ofNodupList`, `ofSurjective`, `ofUnique`, `pempty`, `prod`, `punit`, `sum`, `toList`, `enum`, `finEnum`, `pfunFinEnum`, `instFinEnum`	35
Theorems `mem_enum`, `card_eq_fintypeCard`, `card_eq_one`, `card_eq_zero`, `card_eq_zero_iff`, `card_fin`, `card_ne_zero`, `card_pos`, `card_pos_iff`, `card_ulift`, `card_unique`, `down_equiv_symm`, `equiv_down`, `equiv_up`, `mem_toList`, `nodup_toList`, `up_equiv_symm`, `mem_enum`, `mem_pi_toList`	19
Total	54

FinEnum

Definitions

Name	Category	Theorems
`card` 📖	CompOp	13 math math: `card_fin`, `equiv_up`, `card_pos`, `down_equiv_symm`, `up_equiv_symm`, `card_pos_iff`, `card_eq_zero_iff`, `card_eq_one`, `equiv_down`, `card_eq_zero`, `card_ulift`, `card_unique`, `card_eq_fintypeCard`
`decEq` 📖	CompOp	1 math math: `List.mem_pi_toList`
`empty` 📖	CompOp	—
`equiv` 📖	CompOp	4 math math: `equiv_up`, `down_equiv_symm`, `up_equiv_symm`, `equiv_down`
`fin` 📖	CompOp	1 math math: `recEmptyOption_of_card_pos`
`instFintype` 📖	CompOp	—
`instSigma` 📖	CompOp	—
`instSubtypeMemListOfDecidableEq` 📖	CompOp	—
`instUnique` 📖	CompOp	—
`instUniqueOfIsEmpty` 📖	CompOp	—
`ofEquiv` 📖	CompOp	—
`ofInjective` 📖	CompOp	—
`ofIsEmpty` 📖	CompOp	—
`ofList` 📖	CompOp	—
`ofNodupList` 📖	CompOp	—
`ofSurjective` 📖	CompOp	—
`ofUnique` 📖	CompOp	—
`pempty` 📖	CompOp	—
`prod` 📖	CompOp	—
`punit` 📖	CompOp	—
`sum` 📖	CompOp	—
`toList` 📖	CompOp	3 math math: `mem_toList`, `nodup_toList`, `List.mem_pi_toList`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_eq_fintypeCard` 📖	mathematical	—	`card` `Fintype.card`	—	`Fin.equiv_iff_eq`
`card_eq_one` 📖	mathematical	—	`card`	—	`card_eq_fintypeCard` `Fintype.card_eq_one_iff_nonempty_unique`
`card_eq_zero` 📖	mathematical	—	`card`	—	`card_eq_zero_iff`
`card_eq_zero_iff` 📖	mathematical	—	`card` `IsEmpty`	—	`card_eq_fintypeCard` `Fintype.card_eq_zero_iff`
`card_fin` 📖	mathematical	—	`card`	—	`Fin.equiv_iff_eq`
`card_ne_zero` 📖	—	—	—	—	`LT.lt.ne'` `card_pos`
`card_pos` 📖	mathematical	—	`card`	—	`card_pos_iff`
`card_pos_iff` 📖	mathematical	—	`card`	—	`Fintype.card_pos_iff` `card_eq_fintypeCard`
`card_ulift` 📖	mathematical	—	`card`	—	`Fin.equiv_iff_eq`
`card_unique` 📖	mathematical	—	`card`	—	`card_eq_fintypeCard` `Fintype.card_congr'`
`down_equiv_symm` 📖	mathematical	—	`DFunLike.coe` `Equiv` `card` `ULift.instFinEnum` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `equiv`	—	—
`equiv_down` 📖	mathematical	—	`DFunLike.coe` `Equiv` `card` `EquivLike.toFunLike` `Equiv.instEquivLike` `equiv` `ULift.instFinEnum`	—	—
`equiv_up` 📖	mathematical	—	`DFunLike.coe` `Equiv` `card` `ULift.instFinEnum` `EquivLike.toFunLike` `Equiv.instEquivLike` `equiv`	—	—
`mem_toList` 📖	mathematical	—	`toList`	—	`Equiv.symm_apply_apply`
`nodup_toList` 📖	mathematical	—	`toList`	—	`List.Nodup.map` `Equiv.injective`
`up_equiv_symm` 📖	mathematical	—	`DFunLike.coe` `Equiv` `card` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `equiv` `ULift.instFinEnum`	—	—

FinEnum.Finset

Definitions

Name	Category	Theorems
`enum` 📖	CompOp	1 math math: `mem_enum`
`finEnum` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mem_enum` 📖	mathematical	—	`Finset` `enum`	—	`Finset.insert_erase`

FinEnum.PSigma

Definitions

Name	Category	Theorems
`finEnum` 📖	CompOp	—
`finEnumPropLeft` 📖	CompOp	—
`finEnumPropProp` 📖	CompOp	—
`finEnumPropRight` 📖	CompOp	—

FinEnum.Quotient

Definitions

Name	Category	Theorems
`enum` 📖	CompOp	—

FinEnum.Subtype

Definitions

Name	Category	Theorems
`finEnum` 📖	CompOp	—

List

Definitions

Name	Category	Theorems
`pfunFinEnum` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mem_pi_toList` 📖	mathematical	—	`pi` `FinEnum.decEq` `FinEnum.toList`	—	`mem_pi` `FinEnum.mem_toList`

List.Pi

Definitions

Name	Category	Theorems
`enum` 📖	CompOp	1 math math: `mem_enum`
`finEnum` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mem_enum` 📖	mathematical	—	`enum`	—	`FinEnum.mem_toList` `List.mem_pi_toList`

ULift

Definitions

Name	Category	Theorems
`instFinEnum` 📖	CompOp	5 math math: `FinEnum.recEmptyOption_of_card_pos`, `FinEnum.equiv_up`, `FinEnum.down_equiv_symm`, `FinEnum.up_equiv_symm`, `FinEnum.equiv_down`

(root)

Definitions

Name	Category	Theorems
`FinEnum` 📖	CompData	—

---

← Back to Index