disjoint_supp_of_notMem

Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents

URI: https://scilib.ai/kg/mathlib#SimpleGraph.ConnectedComponent.Represents.disjoint_supp_of_notMem

← MathLib Explorer

English

If hrep represents s and C, then s.ncard = C.ncard.

Русский

Если s представляет C, то кардинал s равен кардиналу C.

LaTeX

$$$ s.ncard = C.ncard $$$

Lean4

theorem disjoint_supp_of_notMem (hrep : Represents s C) (h : c ∉ C) : Disjoint s c.supp :=
  by
  rw [Set.disjoint_left]
  intro a ha hc
  simp only [mem_supp_iff] at hc
  subst hc
  exact h (hrep.1 ha)

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

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

Разделы

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

Аффилиация

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