edgeSet_eq_setOf_exists_isLink — Mathlib

English

The edge set E(G) is exactly the set of edges e for which there exist vertices x and y with G.IsLink e x y.

Русский

Множество ребер E(G) равно множеству ребер e, для которых существует пара вершин x, y с G.IsLink e x y.

LaTeX

$$$E(G) = \\{ e \\mid \\exists x \\exists y\\; G.IsLink\\,e\\,x\\,y \\}$$$

Lean4

theorem edgeSet_eq_setOf_exists_isLink : E(G) = {e | ∃ x y, G.IsLink e x y} :=
  Set.ext G.edge_mem_iff_exists_isLink

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