componentCompl_nonempty_of_infinite

English

Let V be an infinite set and G a simple graph on V. For every finite subset K ⊆ V, there exists a nonempty component of the graph obtained by removing K from V; i.e., the set of components outside K is nonempty.

Русский

Пусть V бесконечно, задан граф G на V. Для любого конечного подмножества K ⊆ V существует непустой компонент графа, полученного вычеркиванием K из V; т.е. множества компонент вне K непусты.

LaTeX

$$$$ \operatorname{Nonempty}(G.\operatorname{ComponentCompl}(K)) $$$$

Lean4

/-- In an infinite graph, the set of components out of a finite set is nonempty. -/
instance componentCompl_nonempty_of_infinite (G : SimpleGraph V) [Infinite V] (K : Finset V) :
    Nonempty (G.ComponentCompl K) :=
  let ⟨_, kK⟩ := K.finite_toSet.infinite_compl.nonempty
  ⟨componentComplMk _ kK⟩

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