ncard_sdiff_of_notMem

Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents

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

← MathLib Explorer

English

Same as previous: if c ∉ C, then (c.supp \\ s).ncard = c.supp.ncard.

Русский

То же самое: если c ∉ C, то (c.supp \\ s).ncard = c.supp.ncard.

LaTeX

$$$ (c.supp \\ s).ncard = c.supp.ncard $$$

Lean4

theorem ncard_sdiff_of_notMem (hrep : Represents s C) (h : c ∉ C) : (c.supp \ s).ncard = c.supp.ncard := by
  rw [(disjoint_supp_of_notMem hrep h).sdiff_eq_right]

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

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

Разделы

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

Аффилиация

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