Commit 2024-11-04 21:20 14b6bcc7

View on Github →

feat(Combinatorics/SimpleGraph): conversions between SimpleGraph and Digraphs (#16954) And proves some lemmas about them. This is a first step to start porting the material of the SimpleGraph part of the library into Digraphs.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Combinatorics/Digraph/Orientation.lean

added def Digraph.toSimpleGraphInclusive

added theorem Digraph.toSimpleGraphInclusive_bot

added theorem Digraph.toSimpleGraphInclusive_mono

added theorem Digraph.toSimpleGraphInclusive_top

added def Digraph.toSimpleGraphStrict

added theorem Digraph.toSimpleGraphStrict_bot

added theorem Digraph.toSimpleGraphStrict_mono

added theorem Digraph.toSimpleGraphStrict_subgraph_toSimpleGraphInclusive

added theorem Digraph.toSimpleGraphStrict_top