ncard_sdiff_of_mem

Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents

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

← MathLib Explorer

English

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_mem (hrep : Represents s C) (h : c ∈ C) : (c.supp \ s).ncard = c.supp.ncard - 1 :=
  by
  obtain ⟨a, ha⟩ := exists_inter_eq_singleton hrep h
  rw [← Set.diff_inter_self_eq_diff, ha, Set.ncard_diff, Set.ncard_singleton]
  simp [← ha]

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

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

Разделы

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

Аффилиация

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