toSimpleGraphStrict_bot — Mathlib

English

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

Русский

Строгий простой граф нижнего ориентированного графа на V совпадает с нижним простым графом на V.

LaTeX

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

Lean4

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

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