Documentation Verification Report

Triplewise

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

Statistics

Metric	Count
Definitions `Triplewise`	1
Theorems `imp`, `map`, `of_map`, `triplewise_append`, `triplewise_cons`, `triplewise_iff`, `triplewise_iff_getElem`, `triplewise_map`, `triplewise_pair`, `triplewise_reverse`, `triplewise_singleton`, `triplewise_triple`	12
Total	13

List

Definitions

Name	Category	Theorems
`Triplewise` 📖	CompData	13 math math: `triplewise_append`, `triplewise_cons`, `Triplewise.of_map`, `triplewise_triple`, `triplewise_map`, `sbtw_iff_triplewise_and_ne_pair`, `triplewise_reverse`, `triplewise_iff`, `triplewise_pair`, `Triplewise.imp`, `triplewise_singleton`, `triplewise_iff_getElem`, `Triplewise.map`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`triplewise_append` 📖	mathematical	—	`Triplewise`	—	—
`triplewise_cons` 📖	mathematical	—	`Triplewise`	—	—
`triplewise_iff` 📖	mathematical	—	`Triplewise`	—	—
`triplewise_iff_getElem` 📖	mathematical	—	`Triplewise`	—	—
`triplewise_map` 📖	mathematical	—	`Triplewise`	—	—
`triplewise_pair` 📖	mathematical	—	`Triplewise`	—	—
`triplewise_reverse` 📖	mathematical	—	`Triplewise`	—	—
`triplewise_singleton` 📖	mathematical	—	`Triplewise`	—	—
`triplewise_triple` 📖	mathematical	—	`Triplewise`	—	—

List.Triplewise

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`imp` 📖	mathematical	`List.Triplewise`	`List.Triplewise`	—	—
`map` 📖	mathematical	`List.Triplewise`	`List.Triplewise`	—	`List.triplewise_map` `imp`
`of_map` 📖	mathematical	`List.Triplewise`	`List.Triplewise`	—	`imp` `List.triplewise_map`

---

← Back to Index