Documentation Verification Report

Hasse

📁 Source: Mathlib/Combinatorics/SimpleGraph/Hasse.lean

Statistics

Metric	Count
Definitions `pathGraphCopy`, `pathGraphIsoToSubgraph`, `pathGraphHom`, `pathGraphHomToSubgraph`, `hasse`, `hasseDualIso`, `pathGraph`	7
Theorems `isContained_pathGraph`, `hasseDualIso_apply`, `hasseDualIso_symm_apply`, `hasse_adj`, `hasse_preconnected_of_pred`, `hasse_preconnected_of_succ`, `hasse_prod`, `pathGraph_adj`, `pathGraph_connected`, `pathGraph_preconnected`, `pathGraph_two_eq_top`	11
Total	18

SimpleGraph

Definitions

Name	Category	Theorems
`hasse` 📖	CompOp	6 math math: `hasse_preconnected_of_pred`, `hasseDualIso_apply`, `hasse_prod`, `hasse_preconnected_of_succ`, `hasse_adj`, `hasseDualIso_symm_apply`
`hasseDualIso` 📖	CompOp	2 math math: `hasseDualIso_apply`, `hasseDualIso_symm_apply`
`pathGraph` 📖	CompOp	7 math math: `pathGraph_adj`, `pathGraph_connected`, `pathGraph_two_eq_top`, `pathGraph_preconnected`, `pathGraph_le_cycleGraph`, `Walk.IsPath.isContained_pathGraph`, `chromaticNumber_pathGraph`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasseDualIso_apply` 📖	mathematical	—	`DFunLike.coe` `Iso` `OrderDual` `hasse` `OrderDual.instPreorder` `RelIso.instFunLike` `Adj` `hasseDualIso` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.ofDual`	—	—
`hasseDualIso_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Iso` `OrderDual` `hasse` `OrderDual.instPreorder` `RelIso.instFunLike` `Adj` `Iso.symm` `hasseDualIso` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual`	—	—
`hasse_adj` 📖	mathematical	—	`Adj` `hasse` `CovBy` `Preorder.toLT`	—	—
`hasse_preconnected_of_pred` 📖	mathematical	—	`Preconnected` `hasse` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`reachable_iff_reflTransGen` `Relation.reflTransGen_swap` `reflTransGen_of_pred` `Order.pred_covBy_of_not_isMin` `LT.lt.not_isMin`
`hasse_preconnected_of_succ` 📖	mathematical	—	`Preconnected` `hasse` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`reachable_iff_reflTransGen` `reflTransGen_of_succ` `Order.covBy_succ_of_not_isMax` `LT.lt.not_isMax`
`hasse_prod` 📖	mathematical	—	`hasse` `Prod.instPreorder` `PartialOrder.toPreorder` `boxProd`	—	`ext`
`pathGraph_adj` 📖	mathematical	—	`Adj` `pathGraph`	—	—
`pathGraph_connected` 📖	mathematical	—	`Connected` `pathGraph`	—	`pathGraph_preconnected`
`pathGraph_preconnected` 📖	mathematical	—	`Preconnected` `pathGraph`	—	`hasse_preconnected_of_succ` `WellFoundedGT.toIsSuccArchimedean` `IsWellOrder.toIsWellFounded` `isWellOrder_gt` `Finite.to_wellFoundedGT` `Finite.of_fintype`
`pathGraph_two_eq_top` 📖	mathematical	—	`pathGraph` `Top.top` `SimpleGraph` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `completeAtomicBooleanAlgebra`	—	`ext` `Fintype.complete` `zero_add` `Nat.instCharZero` `Nat.instAtLeastTwoHAddOfNat` `Fin.instNeZeroHAddNatOfNat_mathlib_1`

SimpleGraph.Walk

Definitions

Name	Category	Theorems
`pathGraphHom` 📖	CompOp	—
`pathGraphHomToSubgraph` 📖	CompOp	—

SimpleGraph.Walk.IsPath

Definitions

Name	Category	Theorems
`pathGraphCopy` 📖	CompOp	—
`pathGraphIsoToSubgraph` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isContained_pathGraph` 📖	mathematical	`SimpleGraph.Walk.IsPath`	`SimpleGraph.IsContained` `SimpleGraph.Walk.length` `SimpleGraph.pathGraph`	—	—

---

← Back to Index