le_induce_union_right — Mathlib

English

Let G be a simple graph on a vertex set V, and let G' be a subgraph of G. For any two vertex sets s, s' ⊆ V, the induced subgraph of G' on s' is contained in the induced subgraph of G' on s ∪ s'. In symbols: G'.induce(s') ⊆ G'.induce(s ∪ s').

Русский

Пусть G − простой граф на вершинном множестве V, G' — подграф G. Для любых множеств вершин s, s' ⊆ V выполнено: индуцированный подграф G' на s' содержится в индуцированном подграфе G' на s ∪ s'.

LaTeX

$$$ G'.induce(s') \le G'.induce(s \cup s') $$$

Lean4

theorem le_induce_union_right : G'.induce s' ≤ G'.induce (s ∪ s') := by exact (sup_le_iff.mp le_induce_union).2

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