Commit 2026-10-12 15:45 1afbf2aa

View on Github →

feat(Combinatorics/SimpleGraph/Hasse): more properties of Hasse graphs of linear orders (#40728)

two forms of an intermediate value theorem for linear orders
the Hasse graph of a linear order is acyclic
a path graph is locally finite

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Acyclic.lean

added theorem SimpleGraph.isAcyclic_hasse_of_linearOrder

added theorem SimpleGraph.isAcyclic_pathGraph

added theorem SimpleGraph.isTree_pathGraph

added theorem SimpleGraph.isTree_pathGraph_add_one

Modified Mathlib/Combinatorics/SimpleGraph/CycleGraph.lean

added theorem SimpleGraph.connected_cycleGraph_add_one

deleted theorem SimpleGraph.cycleGraph_connected

deleted theorem SimpleGraph.cycleGraph_preconnected

added theorem SimpleGraph.preconnected_cycleGraph

Modified Mathlib/Combinatorics/SimpleGraph/Hasse.lean

added theorem SimpleGraph.Walk.mem_darts_hasse_of_ge_of_le_of_le

added theorem SimpleGraph.Walk.mem_support_hasse_of_ge_of_le

added theorem SimpleGraph.connected_pathGraph

added theorem SimpleGraph.connected_pathGraph_add_one

deleted theorem SimpleGraph.hasse_preconnected_of_pred

deleted theorem SimpleGraph.hasse_preconnected_of_succ

deleted theorem SimpleGraph.pathGraph_connected

deleted theorem SimpleGraph.pathGraph_preconnected

added theorem SimpleGraph.preconnected_hasse_of_predOrder

added theorem SimpleGraph.preconnected_hasse_of_succOrder

added theorem SimpleGraph.preconnected_pathGraph

Modified Mathlib/Data/Fintype/Defs.lean

Modified Mathlib/Order/Cover.lean