# 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) [] :

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

Equations
Instances For
@[simp]
theorem SimpleGraph.hasse_adj {α : Type u_1} [] {a : α} {b : α} :
.Adj a b a b b a
def SimpleGraph.hasseDualIso {α : Type u_1} [] :

αᵒᵈ and α have the same Hasse diagram.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem SimpleGraph.hasseDualIso_apply {α : Type u_1} [] (a : αᵒᵈ) :
SimpleGraph.hasseDualIso a = OrderDual.ofDual a
@[simp]
theorem SimpleGraph.hasseDualIso_symm_apply {α : Type u_1} [] (a : α) :
(SimpleGraph.Iso.symm SimpleGraph.hasseDualIso) a = OrderDual.toDual a
@[simp]
theorem SimpleGraph.hasse_prod (α : Type u_1) (β : Type u_2) [] [] :

The path graph on n vertices.

Equations
Instances For
theorem SimpleGraph.pathGraph_adj {n : } {u : Fin n} {v : Fin n} :
.Adj u v u + 1 = v v + 1 = u