edgeFinset_top — Mathlib

English

In the complete graph on V, the edgeFinset consists exactly of all unordered pairs of distinct vertices, i.e., all non-diagonal edges.

Русский

В полном графе на множестве вершин V множество edgeFinset состоит ровно из всех неупорядоченных пар различных вершин, то есть из всех ребер без петель.

LaTeX

$$$ (\top : SimpleGraph V).edgeFinset = \{ e \mid \neg e.IsDiag \} : Finset _ $$$

Lean4

@[simp]
theorem edgeFinset_top [DecidableEq V] : (⊤ : SimpleGraph V).edgeFinset = ({e | ¬e.IsDiag} : Finset _) := by
  simp [← coe_inj]

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