isIndepSet_induce — Mathlib

English

Independence in an induced subgraph corresponds to independence of the image in G.

Русский

Независимость в индуцированном подграфе эквивалентна независимости образа в G.

LaTeX

$$$((\\top : Subgraph G).induce F).coe.IsIndepSet s \\iff G.IsIndepSet (\\operatorname{Subtype.val}'' s).$$$

Lean4

/-- The embedding of an independent set of an induced subgraph of the subgraph `G` is an independent
set in `G` and vice versa. -/
theorem isIndepSet_induce {F : Set α} {s : Set F} :
    ((⊤ : Subgraph G).induce F).coe.IsIndepSet s ↔ G.IsIndepSet (Subtype.val '' s) := by simp [Set.Pairwise]

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