notMem_of_mem

Mathlib.Combinatorics.SimpleGraph.Ends.Defs

URI: https://scilib.ai/kg/mathlib#SimpleGraph.ComponentCompl.notMem_of_mem

English

If c is in C (a component outside K), then c is not in K.

Русский

Если вершина c принадлежит компоненте вне K, то c не принадлежит K.

LaTeX

$$$$ c \in C \Rightarrow c \notin K $$$$

Lean4

theorem notMem_of_mem {C : G.ComponentCompl K} {c : V} (cC : c ∈ C) : c ∉ K := fun cK =>
  Set.disjoint_iff.mp C.disjoint_right ⟨cK, cC⟩

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

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

Разделы

Аффилиация

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