Short

Statistics

Metric	Count
Definitions `ListShort`, `cons`, `Short`, `mk'`, `ofIsEmpty`, `equivDecidable`, `fintypeLeft`, `fintypeLeftMoves`, `fintypeRight`, `fintypeRightMoves`, `leDecidable`, `leLFDecidable`, `lfDecidable`, `listShortGet`, `ltDecidable`, `moveLeftShort`, `moveLeftShort'`, `moveRightShort`, `moveRightShort'`, `short0`, `short1`, `shortAdd`, `shortBit0`, `shortBit1`, `shortNat`, `shortNeg`, `shortOfLists`, `shortOfNat`, `shortOfRelabelling`	29
Theorems `short_birthday`, `subsingleton_short`, `subsingleton_short_example`	3
Total	32

Name	Category	Theorems
`ListShort` 📖	CompData	—
`Short` 📖	CompData	2 math math: `subsingleton_short`, `subsingleton_short_example`
`equivDecidable` 📖	CompOp	—
`fintypeLeft` 📖	CompOp	—
`fintypeLeftMoves` 📖	CompOp	—
`fintypeRight` 📖	CompOp	—
`fintypeRightMoves` 📖	CompOp	—
`leDecidable` 📖	CompOp	—
`leLFDecidable` 📖	CompOp	—
`lfDecidable` 📖	CompOp	—
`listShortGet` 📖	CompOp	—
`ltDecidable` 📖	CompOp	—
`moveLeftShort` 📖	CompOp	—
`moveLeftShort'` 📖	CompOp	—
`moveRightShort` 📖	CompOp	—
`moveRightShort'` 📖	CompOp	—
`short0` 📖	CompOp	—
`short1` 📖	CompOp	—
`shortAdd` 📖	CompOp	—
`shortBit0` 📖	CompOp	—
`shortBit1` 📖	CompOp	—
`shortNat` 📖	CompOp	—
`shortNeg` 📖	CompOp	—
`shortOfLists` 📖	CompOp	—
`shortOfNat` 📖	CompOp	—
`shortOfRelabelling` 📖	CompOp	—

Name	Kind	Assumes	Proves	Validates	Depends On
`short_birthday` 📖	mathematical	—	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `Ordinal.partialOrder` `birthday` `Ordinal.omega0`	—	`birthday.eq_1` `max_lt_iff` `Cardinal.ord_aleph0` `Cardinal.lsub_lt_ord_of_isRegular` `Cardinal.isRegular_aleph0` `Cardinal.lt_aleph0_of_finite` `Finite.of_fintype`
`subsingleton_short` 📖	mathematical	—	`Short`	—	`Lean.Meta.FastSubsingleton.elim` `Fintype.instFastSubsingleton` `Lean.Meta.instFastSubsingletonForall`
`subsingleton_short_example` 📖	mathematical	—	`Short`	—	`Lean.Meta.FastSubsingleton.elim` `Fintype.instFastSubsingleton` `Subsequent.mk_left` `Subsequent.mk_right`

Name	Category	Theorems
`cons` 📖	CompOp	—

Name	Category	Theorems
`mk'` 📖	CompOp	—
`ofIsEmpty` 📖	CompOp	—

---