Documentation Verification Report

Shortlex

📁 Source: Mathlib/Data/List/Shortlex.lean

Statistics

Metric	Count
Definitions `Shortlex`	1
Theorems `append_left`, `append_right`, `asymm`, `cons`, `of_cons`, `of_length_lt`, `of_lex`, `trichotomous`, `wf`, `not_shortlex_nil_right`, `shortlex_cons_iff`, `shortlex_def`, `shortlex_iff_lex`, `shortlex_nil_or_eq_nil`, `shortlex_singleton_iff`	15
Total	16

List

Definitions

Name	Category	Theorems
`Shortlex` 📖	MathDef	11 math math: `Shortlex.of_lex`, `shortlex_singleton_iff`, `shortlex_nil_or_eq_nil`, `not_shortlex_nil_right`, `shortlex_def`, `Shortlex.of_length_lt`, `shortlex_cons_iff`, `Shortlex.trichotomous`, `Shortlex.asymm`, `Shortlex.wf`, `shortlex_iff_lex`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`not_shortlex_nil_right` 📖	mathematical	—	`Shortlex`	—	`shortlex_def`
`shortlex_cons_iff` 📖	mathematical	—	`Shortlex`	—	`IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le`
`shortlex_def` 📖	mathematical	—	`Shortlex`	—	—
`shortlex_iff_lex` 📖	mathematical	—	`Shortlex`	—	—
`shortlex_nil_or_eq_nil` 📖	mathematical	—	`Shortlex`	—	`Shortlex.of_length_lt`
`shortlex_singleton_iff` 📖	mathematical	—	`Shortlex`	—	—

List.Shortlex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`append_left` 📖	—	`List.Shortlex`	—	—	`List.shortlex_def` `of_length_lt` `of_lex` `AddRightCancelSemigroup.toIsRightCancelAdd` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `List.Lex.append_left`
`append_right` 📖	—	`List.Shortlex`	—	—	`List.shortlex_def` `of_length_lt`
`asymm` 📖	mathematical	—	`List.Shortlex`	—	`InvImage.asymm` `Prod.instAsymmLex_mathlib` `instAsymmLt` `List.Lex.asymm`
`cons` 📖	—	`List.Shortlex`	—	—	`List.shortlex_cons_iff`
`of_cons` 📖	—	`List.Shortlex`	—	—	`List.shortlex_cons_iff`
`of_length_lt` 📖	mathematical	—	`List.Shortlex`	—	—
`of_lex` 📖	mathematical	—	`List.Shortlex`	—	—
`trichotomous` 📖	mathematical	—	`List.Shortlex`	—	`InvImage.trichotomous` `Prod.trichotomous` `List.Lex.trichotomous`
`wf` 📖	mathematical	—	`List.Shortlex`	—	`List.not_shortlex_nil_right` `List.exists_of_length_succ` `le_rfl` `AddRightCancelSemigroup.toIsRightCancelAdd`

---

← Back to Index