Commit 2023-03-06 07:14 fa0f201c

View on Github →

feat: port Combinatorics.SimpleGraph.Hasse (#2582)

depends on: #2565

Estimated changes

Modified Mathlib.lean

Created Mathlib/Combinatorics/SimpleGraph/Hasse.lean

added def SimpleGraph.hasse

added def SimpleGraph.hasseDualIso

added theorem SimpleGraph.hasseDualIso_apply

added theorem SimpleGraph.hasseDualIso_symm_apply

added theorem SimpleGraph.hasse_adj

added theorem SimpleGraph.hasse_preconnected_of_pred

added theorem SimpleGraph.hasse_preconnected_of_succ

added theorem SimpleGraph.hasse_prod

added def SimpleGraph.pathGraph

added theorem SimpleGraph.pathGraph_connected

added theorem SimpleGraph.pathGraph_preconnected