Destutter

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

Statistics

Metric	Count
Definitions	0
Theorems `length_le_length_destutter`, `length_le_length_destutter_ne`, `destutter_eq_dedup`, `destutter'_cons`, `destutter'_cons_neg`, `destutter'_cons_pos`, `destutter'_eq_self_iff`, `destutter'_is_chain`, `destutter'_is_chain'`, `destutter'_ne_nil`, `destutter'_nil`, `destutter'_of_chain`, `destutter'_of_isChain_cons`, `destutter'_singleton`, `destutter'_sublist`, `destutter_cons'`, `destutter_cons_cons`, `destutter_eq_nil`, `destutter_eq_self_iff`, `destutter_idem`, `destutter_is_chain'`, `destutter_nil`, `destutter_of_chain'`, `destutter_of_isChain`, `destutter_pair`, `destutter_singleton`, `destutter_sublist`, `isChain_cons_destutter'_of_rel`, `isChain_destutter`, `isChain_destutter'`, `le_length_destutter'_cons`, `length_destutter'_congr`, `length_destutter'_cotrans_ge`, `length_destutter_le_length_destutter_cons`, `length_destutter_ne_le_length_destutter_cons`, `map_destutter`, `map_destutter_ne`, `mem_destutter'`	38
Total	38

List

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`destutter'_cons` 📖	mathematical	—	`destutter'`	—	—
`destutter'_cons_neg` 📖	mathematical	—	`destutter'`	—	`destutter'.eq_2`
`destutter'_cons_pos` 📖	mathematical	—	`destutter'`	—	`destutter'.eq_2`
`destutter'_eq_self_iff` 📖	mathematical	—	`destutter'`	—	`isChain_destutter'` `destutter'_of_isChain_cons`
`destutter'_is_chain` 📖	mathematical	—	`destutter'`	—	`isChain_cons_destutter'_of_rel`
`destutter'_is_chain'` 📖	mathematical	—	`destutter'`	—	`isChain_destutter'`
`destutter'_ne_nil` 📖	—	—	—	—	`mem_destutter'`
`destutter'_nil` 📖	mathematical	—	`destutter'`	—	—
`destutter'_of_chain` 📖	mathematical	—	`destutter'`	—	`destutter'_of_isChain_cons`
`destutter'_of_isChain_cons` 📖	mathematical	—	`destutter'`	—	`destutter'_cons_pos`
`destutter'_singleton` 📖	mathematical	—	`destutter'`	—	—
`destutter'_sublist` 📖	mathematical	—	`destutter'`	—	`destutter'.eq_2` `Sublist.cons_cons`
`destutter_cons'` 📖	mathematical	—	`destutter` `destutter'`	—	—
`destutter_cons_cons` 📖	mathematical	—	`destutter` `destutter'`	—	—
`destutter_eq_nil` 📖	mathematical	—	`destutter`	—	`destutter'_ne_nil`
`destutter_eq_self_iff` 📖	mathematical	—	`destutter`	—	`destutter'_eq_self_iff`
`destutter_idem` 📖	mathematical	—	`destutter`	—	`destutter_of_isChain` `isChain_destutter`
`destutter_is_chain'` 📖	mathematical	—	`destutter`	—	`isChain_destutter`
`destutter_nil` 📖	mathematical	—	`destutter`	—	—
`destutter_of_chain'` 📖	mathematical	—	`destutter`	—	`destutter_of_isChain`
`destutter_of_isChain` 📖	mathematical	—	`destutter`	—	`destutter'_of_isChain_cons`
`destutter_pair` 📖	mathematical	—	`destutter`	—	`destutter_cons_cons`
`destutter_singleton` 📖	mathematical	—	`destutter`	—	—
`destutter_sublist` 📖	mathematical	—	`destutter`	—	`destutter'_sublist`
`isChain_cons_destutter'_of_rel` 📖	mathematical	—	`destutter'`	—	`destutter'_cons_pos` `isChain_destutter'`
`isChain_destutter` 📖	mathematical	—	`destutter`	—	`isChain_destutter'`
`isChain_destutter'` 📖	mathematical	—	`destutter'`	—	`destutter'_singleton`
`le_length_destutter'_cons` 📖	mathematical	—	`destutter'`	—	`destutter'_cons_pos` `destutter'_cons_neg` `em` `trans` `IsPreorder.toIsTrans` `IsEquiv.toIsPreorder` `symm` `IsEquiv.toSymm` `Eq.ge` `length_destutter'_congr`
`length_destutter'_congr` 📖	mathematical	—	`destutter'`	—	`LE.le.antisymm` `length_destutter'_cotrans_ge` `IsPreorder.toIsTrans` `IsEquiv.toIsPreorder` `symm` `IsEquiv.toSymm`
`length_destutter'_cotrans_ge` 📖	mathematical	—	`destutter'`	—	`trans`
`length_destutter_le_length_destutter_cons` 📖	mathematical	—	`destutter`	—	`le_length_destutter'_cons`
`length_destutter_ne_le_length_destutter_cons` 📖	mathematical	—	`destutter`	—	`length_destutter_le_length_destutter_cons` `Ne.instIsEquiv_compl`
`map_destutter` 📖	mathematical	—	`destutter`	—	—
`map_destutter_ne` 📖	mathematical	—	`destutter`	—	`map_destutter`
`mem_destutter'` 📖	mathematical	—	`destutter'`	—	`destutter'.eq_2`

List.IsChain

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`length_le_length_destutter` 📖	mathematical	—	`List.destutter`	—	—
`length_le_length_destutter_ne` 📖	mathematical	—	`List.destutter`	—	`length_le_length_destutter` `Ne.instIsEquiv_compl`

List.Pairwise

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`destutter_eq_dedup` 📖	mathematical	—	`List.destutter` `List.dedup`	—	—

---

← Back to Index