The Hasse diagram as a graph

This file defines the Hasse diagram of an order (graph of CovBy, the covering relation) and the path graph on n vertices.

Main declarations

• SimpleGraph.hasse: Hasse diagram of an order.
• SimpleGraph.pathGraph: Path graph on n vertices.

def SimpleGraph.hasse (α : Type u_1) [Preorder α] : SimpleGraph α

The Hasse diagram of an order as a simple graph. The graph of the covering relation.

Equations

• SimpleGraph.hasse α = { Adj := fun (a b : α) => a ⋖ b ∨ b ⋖ a, symm := ⋯, loopless := ⋯ }

@[simp]

theorem SimpleGraph.hasse_adj {α : Type u_1} [Preorder α] {a b : α} : (hasse α).Adj a b ↔ a ⋖ b ∨ b ⋖ a

@[instance_reducible]

instance SimpleGraph.instDecidableRelAdjHasseOfFintypeOfDecidableLT {α : Type u_1} [Preorder α] [Fintype α] [DecidableLT α] : DecidableRel (hasse α).Adj

Equations

• SimpleGraph.instDecidableRelAdjHasseOfFintypeOfDecidableLT x✝¹ x✝ = decidable_of_iff' (x✝¹ ⋖ x✝ ∨ x✝ ⋖ x✝¹) ⋯

def SimpleGraph.hasseDualIso {α : Type u_1} [Preorder α] : hasse αᵒᵈ ≃g hasse α

αᵒᵈ and α have the same Hasse diagram.

Equations

• SimpleGraph.hasseDualIso = { toEquiv := OrderDual.ofDual, map_rel_iff' := ⋯ }

@[simp]

theorem SimpleGraph.hasseDualIso_apply {α : Type u_1} [Preorder α] (a : αᵒᵈ) : hasseDualIso a = OrderDual.ofDual a

@[simp]

theorem SimpleGraph.hasseDualIso_symm_apply {α : Type u_1} [Preorder α] (a : α) : hasseDualIso.symm a = OrderDual.toDual a

theorem SimpleGraph.cliqueFree_hasse_three {α : Type u_1} [Preorder α] : (hasse α).CliqueFree 3

The Hasse diagram of a preorder is triangle-free. This is the graph-theoretic formulation of not_covBy_of_lt_of_lt: if a ⋖ b and b ⋖ c then ¬a ⋖ c.

@[simp]

theorem SimpleGraph.hasse_prod (α : Type u_1) (β : Type u_2) [PartialOrder α] [PartialOrder β] : hasse (α × β) = hasse α □ hasse β

theorem SimpleGraph.Walk.mem_support_hasse_of_ge_of_le (α : Type u_1) [LinearOrder α] {u v : α} (w : (hasse α).Walk u v) {x : α} (hu : u ≤ x) (hv : x ≤ v) : x ∈ w.support

A discrete form of the intermediate value theorem – a walk in a linear graph visits all of the vertices between its endpoints.

theorem SimpleGraph.Walk.mem_darts_hasse_of_ge_of_le_of_le (α : Type u_1) [LinearOrder α] {u v : α} (w : (hasse α).Walk u v) {d : (hasse α).Dart} (hu : u ≤ d.toProd.1) (hd : d.toProd.1 ≤ d.toProd.2) (hv : d.toProd.2 ≤ v) : d ∈ w.darts

A discrete form of the intermediate value theorem – a walk in a linear graph visits all of the darts between its endpoints, oriented from the walk's start to its end.

theorem SimpleGraph.preconnected_hasse_of_succOrder (α : Type u_1) [LinearOrder α] [SuccOrder α] [IsSuccArchimedean α] : (hasse α).Preconnected

@[deprecated SimpleGraph.preconnected_hasse_of_succOrder (since := "2026-10-01")]

theorem SimpleGraph.hasse_preconnected_of_succ (α : Type u_1) [LinearOrder α] [SuccOrder α] [IsSuccArchimedean α] : (hasse α).Preconnected

Alias of SimpleGraph.preconnected_hasse_of_succOrder.

theorem SimpleGraph.preconnected_hasse_of_predOrder (α : Type u_1) [LinearOrder α] [PredOrder α] [IsPredArchimedean α] : (hasse α).Preconnected

@[deprecated SimpleGraph.preconnected_hasse_of_predOrder (since := "2026-10-01")]

theorem SimpleGraph.hasse_preconnected_of_pred (α : Type u_1) [LinearOrder α] [PredOrder α] [IsPredArchimedean α] : (hasse α).Preconnected

Alias of SimpleGraph.preconnected_hasse_of_predOrder.

def SimpleGraph.pathGraph (n : ℕ) : SimpleGraph (Fin n)

The path graph on n vertices.

Equations

• SimpleGraph.pathGraph n = SimpleGraph.hasse (Fin n)

theorem SimpleGraph.pathGraph_adj {n : ℕ} {u v : Fin n} : (pathGraph n).Adj u v ↔ ↑u + 1 = ↑v ∨ ↑v + 1 = ↑u

@[simp]

theorem SimpleGraph.preconnected_pathGraph (n : ℕ) : (pathGraph n).Preconnected

@[deprecated SimpleGraph.preconnected_pathGraph (since := "2026-10-01")]

theorem SimpleGraph.pathGraph_preconnected (n : ℕ) : (pathGraph n).Preconnected

Alias of SimpleGraph.preconnected_pathGraph.

theorem SimpleGraph.connected_pathGraph_add_one (n : ℕ) : (pathGraph (n + 1)).Connected

@[deprecated SimpleGraph.connected_pathGraph_add_one (since := "2026-10-01")]

theorem SimpleGraph.pathGraph_connected (n : ℕ) : (pathGraph (n + 1)).Connected

Alias of SimpleGraph.connected_pathGraph_add_one.

@[simp]

theorem SimpleGraph.connected_pathGraph {n : ℕ} : (pathGraph n).Connected ↔ n ≠ 0

theorem SimpleGraph.pathGraph_two_eq_top : pathGraph 2 = ⊤

@[instance_reducible]

instance SimpleGraph.instDecidableRelFinAdjPathGraph (n : ℕ) : DecidableRel (pathGraph n).Adj

Equations

• SimpleGraph.instDecidableRelFinAdjPathGraph n = SimpleGraph.instDecidableRelFinAdjPathGraph._aux_1 n

theorem SimpleGraph.pathGraph_le_cycleGraph {n : ℕ} : pathGraph n ≤ cycleGraph n

def SimpleGraph.Walk.pathGraphHomToSubgraph {V : Type u_3} {G : SimpleGraph V} {u v : V} (w : G.Walk u v) : pathGraph (w.length + 1) →g w.toSubgraph.coe

The subgraph of a walk contains the path graph with the same number of vertices

Equations

• w.pathGraphHomToSubgraph = { toFun := fun (n : Fin (w.length + 1)) => ⟨w.support[n], ⋯⟩, map_rel' := ⋯ }

def SimpleGraph.Walk.pathGraphHom {V : Type u_3} {G : SimpleGraph V} {u v : V} (w : G.Walk u v) : pathGraph (w.length + 1) →g G

A walk induces a homomorphism from a path graph to the graph

Equations

• w.pathGraphHom = w.toSubgraph.hom.comp w.pathGraphHomToSubgraph

def SimpleGraph.Walk.IsPath.pathGraphIsoToSubgraph {V : Type u_3} [DecidableEq V] {G : SimpleGraph V} {u v : V} {w : G.Walk u v} (hw : w.IsPath) : pathGraph (w.length + 1) ≃g w.toSubgraph.coe

The subgraph of a path is isomorphic to the path graph with the same number of vertices

Equations

• One or more equations did not get rendered due to their size.

def SimpleGraph.Walk.IsPath.pathGraphCopy {V : Type u_3} [DecidableEq V] {G : SimpleGraph V} {u v : V} {w : G.Walk u v} (hw : w.IsPath) : (pathGraph (w.length + 1)).Copy G

A path induces an injective homomorphism from a path graph to the graph

Equations

• hw.pathGraphCopy = w.toSubgraph.coeCopy.comp hw.pathGraphIsoToSubgraph.toCopy

theorem SimpleGraph.Walk.IsPath.isContained_pathGraph {V : Type u_3} {G : SimpleGraph V} {u v : V} {w : G.Walk u v} (hw : w.IsPath) : (pathGraph (w.length + 1)).IsContained G