Documentation Verification Report

Tree

📁 Source: Mathlib/Order/SuccPred/Tree.lean

Statistics

Metric	Count
Definitions `findAtom`, `RootedTree`, `orderBot`, `predOrder`, `semilatticeInf`, `subtree`, `subtreeOf`, `subtrees`, `α`, `SubRootedTree`, `coeTree`, `root`, `instCoeOutSubRootedTreeRootedTree`, `instCoeSortRootedTreeType`, `instSetLikeSubRootedTreeα`	15
Theorems `findAtom_bot`, `findAtom_eq_bot`, `findAtom_le`, `findAtom_ne_bot`, `instIsAtomic`, `isAtom_findAtom`, `isAtom_findAtom_iff`, `pred_findAtom`, `isPredArchimedean`, `mem_subtreeOf`, `mem_subtrees_disjoint_iff`, `root_subtree`, `subtreeOf_mem_subtrees`, `subtree_root`, `subtrees_disjoint`, `bot_mem_iff`, `ext`, `ext_iff`, `mem_iff`, `root_ne_bot_of_mem_subtrees`	20
Total	35

IsPredArchimedean

Definitions

Name	Category	Theorems
`findAtom` 📖	CompOp	6 math math: `isAtom_findAtom`, `pred_findAtom`, `findAtom_eq_bot`, `findAtom_le`, `findAtom_bot`, `isAtom_findAtom_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`findAtom_bot` 📖	mathematical	—	`findAtom` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder`	—	`Function.iterate_fixed` `Order.pred_bot`
`findAtom_eq_bot` 📖	mathematical	—	`findAtom` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder`	—	`LE.le.exists_pred_iterate` `bot_le` `Nat.find_min'` `findAtom.congr_simp` `findAtom_bot`
`findAtom_le` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `findAtom`	—	`Order.pred_iterate_le`
`findAtom_ne_bot` 📖	—	—	—	—	`Iff.not` `findAtom_eq_bot`
`instIsAtomic` 📖	mathematical	—	`IsAtomic`	—	`isAtom_findAtom` `findAtom_le`
`isAtom_findAtom` 📖	mathematical	—	`IsAtom` `PartialOrder.toPreorder` `findAtom`	—	`pred_findAtom` `Order.le_pred_of_lt`
`isAtom_findAtom_iff` 📖	mathematical	—	`IsAtom` `PartialOrder.toPreorder` `findAtom`	—	`findAtom.congr_simp` `findAtom_bot` `isAtom_findAtom`
`pred_findAtom` 📖	mathematical	—	`Order.pred` `PartialOrder.toPreorder` `findAtom` `Bot.bot` `OrderBot.toBot` `Preorder.toLE`	—	`LE.le.exists_pred_iterate` `bot_le` `Nat.find_spec` `Order.pred_bot`

RootedTree

Definitions

Name	Category	Theorems
`orderBot` 📖	CompOp	2 math math: `mem_subtrees_disjoint_iff`, `SubRootedTree.bot_mem_iff`
`predOrder` 📖	CompOp	1 math math: `isPredArchimedean`
`semilatticeInf` 📖	CompOp	4 math math: `mem_subtrees_disjoint_iff`, `isPredArchimedean`, `SubRootedTree.bot_mem_iff`, `SubRootedTree.mem_iff`
`subtree` 📖	CompOp	2 math math: `root_subtree`, `subtree_root`
`subtreeOf` 📖	CompOp	2 math math: `subtreeOf_mem_subtrees`, `mem_subtreeOf`
`subtrees` 📖	CompOp	2 math math: `subtreeOf_mem_subtrees`, `subtrees_disjoint`
`α` 📖	CompOp	5 math math: `isPredArchimedean`, `subtrees_disjoint`, `mem_subtreeOf`, `SubRootedTree.bot_mem_iff`, `SubRootedTree.mem_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isPredArchimedean` 📖	mathematical	—	`IsPredArchimedean` `α` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `semilatticeInf` `predOrder`	—	—
`mem_subtreeOf` 📖	mathematical	—	`α` `SubRootedTree` `SetLike.instMembership` `instSetLikeSubRootedTreeα` `subtreeOf`	—	`isPredArchimedean`
`mem_subtrees_disjoint_iff` 📖	mathematical	`SubRootedTree` `Set` `Set.instMembership` `subtrees` `α` `SetLike.instMembership` `instSetLikeSubRootedTreeα`	`Disjoint` `SemilatticeInf.toPartialOrder` `semilatticeInf` `orderBot`	—	`SubRootedTree.root_ne_bot_of_mem_subtrees` `Disjoint.eq_bot` `Mathlib.Tactic.Contrapose.contrapose₂` `lt_or_le_of_directed` `isPredArchimedean` `SubRootedTree.mem_iff` `bot_lt_iff_ne_bot` `disjoint_iff` `SubRootedTree.ext` `IsAtom.le_iff_eq` `le_total_of_directed` `le_inf_iff`
`root_subtree` 📖	mathematical	—	`SubRootedTree.root` `subtree`	—	—
`subtreeOf_mem_subtrees` 📖	mathematical	—	`SubRootedTree` `Set` `Set.instMembership` `subtrees` `subtreeOf`	—	`isPredArchimedean`
`subtree_root` 📖	mathematical	—	`subtree` `SubRootedTree.root`	—	—
`subtrees_disjoint` 📖	mathematical	—	`Set.PairwiseDisjoint` `Set` `α` `SubRootedTree` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `subtrees` `SetLike.coe` `instSetLikeSubRootedTreeα`	—	`Function.onFun_apply` `Set.disjoint_left` `SubRootedTree.root_ne_bot_of_mem_subtrees` `disjoint_self` `mem_subtrees_disjoint_iff`

SubRootedTree

Definitions

Name	Category	Theorems
`coeTree` 📖	CompOp	—
`root` 📖	CompOp	5 math math: `RootedTree.root_subtree`, `ext_iff`, `RootedTree.subtree_root`, `bot_mem_iff`, `mem_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bot_mem_iff` 📖	mathematical	—	`RootedTree.α` `SubRootedTree` `SetLike.instMembership` `instSetLikeSubRootedTreeα` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `RootedTree.semilatticeInf` `RootedTree.orderBot` `root`	—	—
`ext` 📖	—	`root`	—	—	—
`ext_iff` 📖	mathematical	—	`root`	—	`ext`
`mem_iff` 📖	mathematical	—	`RootedTree.α` `SubRootedTree` `SetLike.instMembership` `instSetLikeSubRootedTreeα` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `RootedTree.semilatticeInf` `root`	—	—
`root_ne_bot_of_mem_subtrees` 📖	—	`SubRootedTree` `Set` `Set.instMembership` `RootedTree.subtrees`	—	—	—

(root)

Definitions

Name	Category	Theorems
`RootedTree` 📖	CompData	—
`SubRootedTree` 📖	CompOp	5 math math: `RootedTree.subtreeOf_mem_subtrees`, `RootedTree.subtrees_disjoint`, `RootedTree.mem_subtreeOf`, `SubRootedTree.bot_mem_iff`, `SubRootedTree.mem_iff`
`instCoeOutSubRootedTreeRootedTree` 📖	CompOp	—
`instCoeSortRootedTreeType` 📖	CompOp	—
`instSetLikeSubRootedTreeα` 📖	CompOp	4 math math: `RootedTree.subtrees_disjoint`, `RootedTree.mem_subtreeOf`, `SubRootedTree.bot_mem_iff`, `SubRootedTree.mem_iff`

---

← Back to Index