The Hasse diagram as a graph #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
This file defines the Hasse diagram of an order (graph of
covby, the covering relation) and the
path graph on
Main declarations #
The Hasse diagram of an order as a simple graph. The graph of the covering relation.
α have the same Hasse diagram.
The path graph on