exists_isLink_of_mem_edgeSet

Mathlib.Combinatorics.Graph.Basic

URI: https://scilib.ai/kg/mathlib#Graph.exists_isLink_of_mem_edgeSet

English

If an edge e lies in the edge set of G, then there exist x and y such that G.IsLink e x y.

Русский

Если ребро e принадлежит множеству ребер G, то существуют x и y такие, что G.IsLink e x y.

LaTeX

$$$e \\in E(G) \\Rightarrow \\exists x\,\\exists y\\, G.IsLink\\,e\\,x\\,y.$$$

Lean4

theorem exists_isLink_of_mem_edgeSet (h : e ∈ E(G)) : ∃ x y, G.IsLink e x y :=
  (edge_mem_iff_exists_isLink ..).1 h

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

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

Разделы

Аффилиация

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