le_card_edgeFinset

Mathlib.Combinatorics.SimpleGraph.DeleteEdges

URI: https://scilib.ai/kg/mathlib#SimpleGraph.DeleteFar.le_card_edgeFinset

English

If G is DeleteFar with p and bottom satisfies p, then r is bounded by the size of the edgeFinset.

Русский

Если G имеет свойство DeleteFar и p выполняется на нижнем, то r ограничено размером edgeFinset.

LaTeX

$$$ G.DeleteFar p r \to p \perp \Rightarrow r \le |G.edgeFinset| $$$

Lean4

theorem le_card_edgeFinset (h : G.DeleteFar p r) (hp : p ⊥) : r ≤ #G.edgeFinset :=
  h subset_rfl (by simpa)

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

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

Разделы

Аффилиация

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