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	15 math math: Shortlex.of_cons, Shortlex.of_lex, shortlex_singleton_iff, shortlex_nil_or_eq_nil, Shortlex.append_right, not_shortlex_nil_right, shortlex_def, Shortlex.of_length_lt, shortlex_cons_iff, Shortlex.cons, Shortlex.trichotomous, Shortlex.append_left, 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 instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Nat.instIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add
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 📖	mathematical	List.Shortlex	List.Shortlex	—	List.shortlex_def of_length_lt of_lex instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Nat.instIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid List.Lex.append_left
append_right 📖	mathematical	List.Shortlex	List.Shortlex	—	List.shortlex_def of_length_lt
asymm 📖	mathematical	—	List.Shortlex	—	—
cons 📖	mathematical	List.Shortlex	List.Shortlex	—	List.shortlex_cons_iff
of_cons 📖	mathematical	List.Shortlex	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 instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Nat.instIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid

---

← Back to Index