instIsEmptyElemForallObjOppositeFinsetComponentComplFunctorEndOfFinite

Mathlib.Combinatorics.SimpleGraph.Ends.Properties

URI: https://scilib.ai/kg/mathlib#SimpleGraph.instIsEmptyElemForallObjOppositeFinsetComponentComplFunctorEndOfFinite

← MathLib Explorer

English

In a finite graph, there are no ends.

Русский

У конечного графа нет концов.

LaTeX

$$$G.end = \\varnothing$$$

Lean4

instance [Finite V] : IsEmpty G.end where
  false := by
    rintro ⟨s, _⟩
    cases nonempty_fintype V
    obtain ⟨v, h⟩ := (s <| Opposite.op Finset.univ).nonempty
    exact Set.disjoint_iff.mp (s _).disjoint_right ⟨by simp only [Finset.coe_univ, Set.mem_univ], h⟩

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

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

Разделы

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

Аффилиация

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