Documentation Verification Report

RelatesInSteps

📁 Source: Cslib/Foundations/Data/RelatesInSteps.lean

Statistics

Metric	Count
Definitions `RelatesInSteps`, `RelatesWithinSteps`	2
Theorems `relatesInSteps`, `apply_le_apply_add`, `head`, `head_induction_on`, `map`, `reflTransGen`, `single`, `succ`, `succ'`, `succ'_iff`, `succ_iff`, `trans`, `zero`, `zero_iff`, `apply_le_apply_add`, `map`, `of_le`, `of_relatesInSteps`, `refl`, `single`, `trans`, `zero`, `zero_iff`	23
Total	25

Relation

Definitions

Name	Category	Theorems
`RelatesInSteps` 📖	CompData	10 math math: `RelatesInSteps.succ'_iff`, `RelatesInSteps.map`, `RelatesInSteps.succ`, `RelatesInSteps.succ'`, `ReflTransGen.relatesInSteps`, `RelatesInSteps.succ_iff`, `RelatesInSteps.zero_iff`, `RelatesInSteps.single`, `RelatesInSteps.trans`, `RelatesInSteps.head`
`RelatesWithinSteps` 📖	MathDef	7 math math: `RelatesWithinSteps.of_le`, `RelatesWithinSteps.zero_iff`, `RelatesWithinSteps.single`, `RelatesWithinSteps.of_relatesInSteps`, `RelatesWithinSteps.trans`, `RelatesWithinSteps.refl`, `RelatesWithinSteps.map`

Relation.ReflTransGen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`relatesInSteps` 📖	mathematical	—	`Relation.RelatesInSteps`	—	—

Relation.RelatesInSteps

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_le_apply_add` 📖	—	`Relation.RelatesInSteps`	—	—	—
`head` 📖	mathematical	`Relation.RelatesInSteps`	`Relation.RelatesInSteps`	—	`single`
`head_induction_on` 📖	—	`Relation.RelatesInSteps` `refl` `head`	—	—	`head`
`map` 📖	mathematical	`Relation.RelatesInSteps`	`Relation.RelatesInSteps`	—	—
`reflTransGen` 📖	—	`Relation.RelatesInSteps`	—	—	—
`single` 📖	mathematical	—	`Relation.RelatesInSteps`	—	—
`succ` 📖	mathematical	`Relation.RelatesInSteps`	`Relation.RelatesInSteps`	—	—
`succ'` 📖	mathematical	`Relation.RelatesInSteps`	`Relation.RelatesInSteps`	—	—
`succ'_iff` 📖	mathematical	—	`Relation.RelatesInSteps`	—	`succ'` `head`
`succ_iff` 📖	mathematical	—	`Relation.RelatesInSteps`	—	`succ`
`trans` 📖	mathematical	`Relation.RelatesInSteps`	`Relation.RelatesInSteps`	—	—
`zero` 📖	—	`Relation.RelatesInSteps`	—	—	—
`zero_iff` 📖	mathematical	—	`Relation.RelatesInSteps`	—	`zero`

Relation.RelatesWithinSteps

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_le_apply_add` 📖	—	`Relation.RelatesWithinSteps`	—	—	`Relation.RelatesInSteps.apply_le_apply_add`
`map` 📖	mathematical	`Relation.RelatesWithinSteps`	`Relation.RelatesWithinSteps`	—	`Relation.RelatesInSteps.map`
`of_le` 📖	mathematical	`Relation.RelatesWithinSteps`	`Relation.RelatesWithinSteps`	—	—
`of_relatesInSteps` 📖	mathematical	`Relation.RelatesInSteps`	`Relation.RelatesWithinSteps`	—	—
`refl` 📖	mathematical	—	`Relation.RelatesWithinSteps`	—	`of_relatesInSteps`
`single` 📖	mathematical	—	`Relation.RelatesWithinSteps`	—	`of_relatesInSteps` `Relation.RelatesInSteps.single`
`trans` 📖	mathematical	`Relation.RelatesWithinSteps`	`Relation.RelatesWithinSteps`	—	`Relation.RelatesInSteps.trans`
`zero` 📖	—	`Relation.RelatesWithinSteps`	—	—	`Relation.RelatesInSteps.zero`
`zero_iff` 📖	mathematical	—	`Relation.RelatesWithinSteps`	—	`zero` `refl`

---

← Back to Index