nonempty

Mathlib.Combinatorics.SimpleGraph.Ends.Defs

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

English

Every component outside K has a nonempty vertex set.

Русский

Каждая компонента вне K содержит по крайней мере одну вершину.

LaTeX

$$$$ (C:\text{ComponentCompl }K).(\text{setLike.coe}) \neq \varnothing $$$$

Lean4

@[simp]
protected theorem nonempty (C : G.ComponentCompl K) : (C : Set V).Nonempty :=
  C.ind fun v vnK => ⟨v, vnK, rfl⟩

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

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

Разделы

Аффилиация

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