toSimpleGraphInclusive_bot — Mathlib

English

The inclusive simple graph of the bottom directed graph on V is the bottom simple graph on V.

Русский

Инклюзивный простой граф нижнего ориентированного графа на V равен нижнему простому графу на V.

LaTeX

$$$ (\\bot_{\\mathrm{Digraph}(V)}).toSimpleGraphInclusive = \\bot_{\\mathrm{SimpleGraph}(V)} $$$

Lean4

@[simp]
theorem toSimpleGraphInclusive_bot : (⊥ : Digraph V).toSimpleGraphInclusive = ⊥ := by ext;
  exact ⟨fun ⟨_, h⟩ ↦ by tauto, False.elim⟩

Похожие утверждения