ncard_inter

Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

theorem ncard_inter (hrep : Represents s C) (h : c ∈ C) : (s ∩ c.supp).ncard = 1 :=
  by
  rw [Set.ncard_eq_one]
  exact exists_inter_eq_singleton hrep h

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

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

Разделы

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

Аффилиация

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