deleteVerts_anti

Mathlib.Combinatorics.SimpleGraph.Subgraph

URI: https://scilib.ai/kg/mathlib#SimpleGraph.Subgraph.deleteVerts_anti

← MathLib Explorer

English

If s ⊆ s', then G'.deleteVerts s' ≤ G'.deleteVerts s.

Русский

Если s ⊆ s', то G'.deleteVerts s' ≤ G'.deleteVerts s.

LaTeX

$$$ (G'.deleteVerts s') \le G'.deleteVerts s \quad \text{whenever } s \subseteq s' $$$

Lean4

@[gcongr, mono]
theorem deleteVerts_anti {s s' : Set V} (h : s ⊆ s') : G'.deleteVerts s' ≤ G'.deleteVerts s :=
  induce_mono (le_refl _) (Set.diff_subset_diff_right h)

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

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

Разделы

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

Аффилиация

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