Documentation Verification Report

Orientation

📁 Source: Mathlib/Combinatorics/Digraph/Orientation.lean

Statistics

Metric	Count
Definitions `toSimpleGraphInclusive`, `toSimpleGraphStrict`	2
Theorems `toSimpleGraphInclusive_bot`, `toSimpleGraphInclusive_mono`, `toSimpleGraphInclusive_top`, `toSimpleGraphStrict_bot`, `toSimpleGraphStrict_mono`, `toSimpleGraphStrict_subgraph_toSimpleGraphInclusive`, `toSimpleGraphStrict_top`	7
Total	9

Digraph

Definitions

Name	Category	Theorems
`toSimpleGraphInclusive` 📖	CompOp	4 math math: `toSimpleGraphInclusive_bot`, `toSimpleGraphInclusive_mono`, `toSimpleGraphInclusive_top`, `toSimpleGraphStrict_subgraph_toSimpleGraphInclusive`
`toSimpleGraphStrict` 📖	CompOp	4 math math: `toSimpleGraphStrict_top`, `toSimpleGraphStrict_mono`, `toSimpleGraphStrict_bot`, `toSimpleGraphStrict_subgraph_toSimpleGraphInclusive`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toSimpleGraphInclusive_bot` 📖	mathematical	—	`toSimpleGraphInclusive` `Bot.bot` `Digraph` `BooleanAlgebra.toBot` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `completeAtomicBooleanAlgebra` `SimpleGraph` `SimpleGraph.completeAtomicBooleanAlgebra`	—	`SimpleGraph.ext`
`toSimpleGraphInclusive_mono` 📖	mathematical	—	`Monotone` `Digraph` `SimpleGraph` `PartialOrder.toPreorder` `instPartialOrder` `SimpleGraph.instPartialOrder` `toSimpleGraphInclusive`	—	—
`toSimpleGraphInclusive_top` 📖	mathematical	—	`toSimpleGraphInclusive` `Top.top` `Digraph` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `completeAtomicBooleanAlgebra` `SimpleGraph` `SimpleGraph.completeAtomicBooleanAlgebra`	—	`SimpleGraph.ext` `SimpleGraph.Adj.ne`
`toSimpleGraphStrict_bot` 📖	mathematical	—	`toSimpleGraphStrict` `Bot.bot` `Digraph` `BooleanAlgebra.toBot` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `completeAtomicBooleanAlgebra` `SimpleGraph` `SimpleGraph.completeAtomicBooleanAlgebra`	—	`SimpleGraph.ext`
`toSimpleGraphStrict_mono` 📖	mathematical	—	`Monotone` `Digraph` `SimpleGraph` `PartialOrder.toPreorder` `instPartialOrder` `SimpleGraph.instPartialOrder` `toSimpleGraphStrict`	—	—
`toSimpleGraphStrict_subgraph_toSimpleGraphInclusive` 📖	mathematical	—	`SimpleGraph` `SimpleGraph.instLE` `toSimpleGraphStrict` `toSimpleGraphInclusive`	—	—
`toSimpleGraphStrict_top` 📖	mathematical	—	`toSimpleGraphStrict` `Top.top` `Digraph` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `completeAtomicBooleanAlgebra` `SimpleGraph` `SimpleGraph.completeAtomicBooleanAlgebra`	—	`SimpleGraph.ext` `SimpleGraph.Adj.ne`

---

← Back to Index