English
Let G be a simple graph on α. For any subset F of α and any finite set s of elements of F, the n-independent-ness of s in the induced subgraph on F is equivalent to the n-independent-ness of its image in G under the natural inclusion.
Русский
Пусть G — простой граф на множестве вершин α. Для любого подмножества F ⊆ α и любого конечного множества s элементов F равносильно тому, чтобы s было n-независимым в индуцированном подграфе на F и чтобы его образ в G через естественную вложенность был n-независимым в G.
LaTeX
$$$((\\top : \\mathrm{Subgraph}(G)).induce F).coe.IsNIndepSet_n(\\uparrow s) \\;\\iff\\; G.IsNIndepSet_n(\\mathrm{Finset.map} \\langle \\mathrm{Subtype.val}, \\mathrm{Subtype.val_injective} \\rangle s)$$$
Lean4
/-- The embedding of an `n`-independent set of an induced subgraph of the subgraph `G` is an
`n`-independent set in `G` and vice versa. -/
theorem isNIndepSet_induce {F : Set α} {s : Finset { x // x ∈ F }} {n : ℕ} :
((⊤ : Subgraph G).induce F).coe.IsNIndepSet n ↑s ↔
G.IsNIndepSet n (Finset.map ⟨Subtype.val, Subtype.val_injective⟩ s) :=
by simp [isNIndepSet_iff, (isIndepSet_induce)]
