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 n vertices.

Main declarations #

simple_graph.hasse: Hasse diagram of an order.
simple_graph.path_graph: Path graph on n vertices.

source

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

simple_graph α

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

Equations

simple_graph.hasse α = {adj := λ (a b : α), a ⋖ b ∨ b ⋖ a, symm := _, loopless := _}

source

@[simp]

theorem simple_graph.hasse_adj {α : Type u_1} [preorder α] {a b : α} :

(simple_graph.hasse α).adj a b ↔ a ⋖ b ∨ b ⋖ a

source

def simple_graph.hasse_dual_iso {α : Type u_1} [preorder α] :

simple_graph.hasse αᵒᵈ ≃g simple_graph.hasse α

αᵒᵈ and α have the same Hasse diagram.

Equations

simple_graph.hasse_dual_iso = {to_equiv := {to_fun := order_dual.of_dual.to_fun, inv_fun := order_dual.of_dual.inv_fun, left_inv := _, right_inv := _}, map_rel_iff' := _}

source

@[simp]

theorem simple_graph.hasse_dual_iso_apply {α : Type u_1} [preorder α] (a : αᵒᵈ) :

⇑simple_graph.hasse_dual_iso a = ⇑order_dual.of_dual a

source

@[simp]

theorem simple_graph.hasse_dual_iso_symm_apply {α : Type u_1} [preorder α] (a : α) :

⇑(simple_graph.hasse_dual_iso.symm) a = ⇑order_dual.to_dual a

source

@[simp]

theorem simple_graph.hasse_prod (α : Type u_1) (β : Type u_2) [partial_order α] [partial_order β] :

simple_graph.hasse (α × β) = simple_graph.hasse α □ simple_graph.hasse β

source

theorem simple_graph.hasse_preconnected_of_succ (α : Type u_1) [linear_order α] [succ_order α] [is_succ_archimedean α] :

(simple_graph.hasse α).preconnected

source

theorem simple_graph.hasse_preconnected_of_pred (α : Type u_1) [linear_order α] [pred_order α] [is_pred_archimedean α] :

(simple_graph.hasse α).preconnected

source

def simple_graph.path_graph (n : ℕ) :

simple_graph (fin n)

The path graph on n vertices.

Equations

simple_graph.path_graph n = simple_graph.hasse (fin n)

source

theorem simple_graph.path_graph_preconnected (n : ℕ) :

(simple_graph.path_graph n).preconnected

source

theorem simple_graph.path_graph_connected (n : ℕ) :

(simple_graph.path_graph (n + 1)).connected