edge_mem_incidenceSet_iff — Mathlib

English

Let G be a simple graph on V. For every edge e in the edge set, e is incident to a iff a is an endpoint of e.

Русский

Пусть G — простой граф на вершины V. Для любого ребра e из множества рёбер графа e инцидентно вершине a тогда и только тогда, когда a является концом e.

LaTeX

$$$e \\in E \\Rightarrow (e \\in \\operatorname{incidenceSet}(a) \\iff a \\in \\{ \\operatorname{fst}(e), \\operatorname{snd}(e) \\})$$$

Lean4

theorem edge_mem_incidenceSet_iff {e : G.edgeSet} : ↑e ∈ G.incidenceSet a ↔ a ∈ (e : Sym2 V) :=
  and_iff_right e.2

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