ncard_eq

Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents

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

English

If hrep represents s and c ∈ C, then (c.supp \\ s).ncard = c.supp.ncard - 1.

Русский

Если s представляет C и c ∈ C, тогда (c.supp \\ s).ncard = c.supp.ncard − 1.

LaTeX

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

Lean4

theorem ncard_eq (hrep : Represents s C) : s.ncard = C.ncard :=
  hrep.image_eq ▸ (Set.ncard_image_of_injOn hrep.injOn).symm

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

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

Разделы

Аффилиация

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