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 #

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

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} [Preorder α] {a : α} {b : α} :

    αᵒᵈ and α have the same Hasse diagram.

    Instances For
      @[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

      The path graph on n vertices.

      Instances For