mathlib documentation

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

def simple_graph.hasse (α : Type u_1) [preorder α] :

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

Equations
@[simp]
theorem simple_graph.hasse_adj {α : Type u_1} [preorder α] {a b : α} :
(simple_graph.hasse α).adj a b a b b a
@[simp]
theorem simple_graph.hasse_prod (α : Type u_1) (β : Type u_2) [partial_order α] [partial_order β] :

The path graph on n vertices.

Equations