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.

@[simp]

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

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

αᵒᵈ and α have the same Hasse diagram.

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

The path graph on n vertices.

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

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