# Documentation

Mathlib.Combinatorics.SimpleGraph.Hasse

# 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.

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

αᵒᵈ and α have the same Hasse diagram.

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.

Instances For