disjoint_right

Mathlib.Combinatorics.SimpleGraph.Ends.Defs

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

English

K is disjoint from any component C outside K.

Русский

K и любая компонента вне K не пересекаются.

LaTeX

$$$$ Disjoint(K, (C:\text{ComponentCompl }K)) $$$$

Lean4

protected theorem disjoint_right (C : G.ComponentCompl K) : Disjoint K C :=
  by
  rw [Set.disjoint_iff]
  exact fun v ⟨vK, vC⟩ => vC.choose vK

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

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

Разделы

Аффилиация

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