nonempty_ends_of_infinite — Mathlib

English

A locally finite preconnected infinite graph has at least one end.

Русский

Локально конечный пре-соединённый бесконечный граф имеет хотя бы один конец.

LaTeX

$$$\\text{End}(G) \\neq \\varnothing$$$

Lean4

/-- A locally finite preconnected infinite graph has at least one end. -/
theorem nonempty_ends_of_infinite [LocallyFinite G] [Fact G.Preconnected] [Infinite V] : G.end.Nonempty := by
  classical apply nonempty_sections_of_finite_inverse_system G.componentComplFunctor

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