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.

Equations
Instances For
    @[simp]
    theorem SimpleGraph.hasse_adj {α : Type u_1} [Preorder α] {a : α} {b : α} :
    (SimpleGraph.hasse α).Adj a b a b b a

    αᵒᵈ and α have the same Hasse diagram.

    Equations
    • SimpleGraph.hasseDualIso = let __src := OrderDual.ofDual; { toEquiv := __src, map_rel_iff' := }
    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.hasseDualIso.symm a = OrderDual.toDual a

      The path graph on n vertices.

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