Documentation Verification Report

Chain

📁 Source: Mathlib/Order/CompleteLattice/Chain.lean

Statistics

Metric	Count
Definitions `ChainClosure`, `maxChain`	2
Theorems `isChain`, `succ_fixpoint`, `succ_fixpoint_iff`, `total`, `chainClosure_empty`, `chainClosure_maxChain`, `maxChain_spec`	7
Total	9

ChainClosure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isChain` 📖	mathematical	`ChainClosure`	`IsChain`	—	`IsChain.succ` `total`
`succ_fixpoint` 📖	mathematical	`ChainClosure` `SuccChain`	`Set` `Set.instHasSubset`	—	`Eq.subset` `Set.instReflSubset` `Set.sUnion_subset`
`succ_fixpoint_iff` 📖	mathematical	`ChainClosure`	`SuccChain` `maxChain`	—	`HasSubset.Subset.antisymm` `Set.instAntisymmSubset` `Set.subset_sUnion_of_mem` `succ_fixpoint` `chainClosure_maxChain` `HasSubset.Subset.antisymm'` `subset_succChain` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Eq.subset` `Set.instReflSubset`
`total` 📖	mathematical	`ChainClosure`	`Set` `Set.instHasSubset`	—	`HasSubset.Subset.trans` `Set.instIsTransSubset` `subset_succChain`

(root)

Definitions

Name	Category	Theorems
`ChainClosure` 📖	CompData	2 math math: `chainClosure_empty`, `chainClosure_maxChain`
`maxChain` 📖	CompOp	3 math math: `maxChain_spec`, `ChainClosure.succ_fixpoint_iff`, `chainClosure_maxChain`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`chainClosure_empty` 📖	mathematical	—	`ChainClosure` `Set` `Set.instEmptyCollection`	—	`Set.notMem_empty` `Set.sUnion_empty`
`chainClosure_maxChain` 📖	mathematical	—	`ChainClosure` `maxChain`	—	—
`maxChain_spec` 📖	mathematical	—	`IsMaxChain` `maxChain`	—	`by_contradiction` `IsChain.superChain_succChain` `ChainClosure.isChain` `chainClosure_maxChain` `HasSSubset.SSubset.ne` `Set.instIrreflSSubset` `ChainClosure.succ_fixpoint_iff`

---

← Back to Index