pairwise_disjoint

Mathlib.Combinatorics.SimpleGraph.Ends.Defs

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

← MathLib Explorer

English

If c ∈ C and d ∉ K and c is adjacent to d, then d ∈ C.

Русский

Если c ∈ C, d ∉ K и c смежна с d, то d ∈ C.

LaTeX

$$$$ c \in C,\ d \notin K,\ G.Adj\ c,d \Rightarrow d \in C $$$$

Lean4

protected theorem pairwise_disjoint : Pairwise fun C D : G.ComponentCompl K => Disjoint (C : Set V) (D : Set V) :=
  by
  rintro C D ne
  rw [Set.disjoint_iff]
  exact fun u ⟨uC, uD⟩ => ne (uC.choose_spec.symm.trans uD.choose_spec)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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