mk'_mem_incidenceSet_left_iff

Mathlib.Combinatorics.SimpleGraph.Basic

URI: https://scilib.ai/kg/mathlib#SimpleGraph.mk'_mem_incidenceSet_left_iff

English

For any G, a, b, we have s(a,b) ∈ incidenceSet a iff Adj a b.

Русский

Для любых G, a, b верно: s(a,b) ∈ incidenceSet a тогда и только тогда, когда Adj a b.

LaTeX

$$$\\forall {V} (G : SimpleGraph V) {a b},\\; s(a,b) \\in G.incidenceSet a \\iff G.Adj a b$$$

Lean4

theorem mk'_mem_incidenceSet_left_iff : s(a, b) ∈ G.incidenceSet a ↔ G.Adj a b :=
  and_iff_left <| Sym2.mem_mk_left _ _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru