toSimpleGraphInclusive_top — Mathlib

English

Let V be a type. The inclusive simple graph obtained from the top directed graph on V is the complete simple graph on V.

Русский

Пусть V — множество вершин. Инклюзивное простого графа, полученное из верхнего ориентированного графа на V, является полным простым графом на V.

LaTeX

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

Lean4

@[simp]
theorem toSimpleGraphInclusive_top : (⊤ : Digraph V).toSimpleGraphInclusive = ⊤ := by ext;
  exact ⟨And.left, fun h ↦ ⟨h.ne, Or.inl trivial⟩⟩

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