English
Let S be a subgraph G and F ⊆ α. If a finite set s of vertices drawn from F forms an n-clique in the subgraph of G induced by F (via S), then the corresponding vertex set in G (obtained by forgetting the subtype) is an n-clique in G.
Русский
Пусть S будет подграфом G и F ⊆ α. Если конечное множество вершин s, взятое из F, образует n-clique в подграфе G, индукированном по F, то соответствующее множество вершин в G образует n-clique в G.
LaTeX
$$$ (S\mathrm{.induce} F).\mathrm{coe}.\mathrm{IsNClique}\,(n, s) \Rightarrow G.\mathrm{IsNClique}\, (n, \mathrm{image} (\mathrm{Subtype.val}, s)). $$$
Lean4
/-- If a set of vertices `A` is an `n`-clique in subgraph of `G` induced by a superset of `A`,
its embedding is an `n`-clique in `G`. -/
theorem of_induce {S : Subgraph G} {F : Set α} {s : Finset { x // x ∈ F }} {n : ℕ}
(cc : (S.induce F).coe.IsNClique n s) : G.IsNClique n (Finset.map ⟨Subtype.val, Subtype.val_injective⟩ s) :=
by
rw [isNClique_iff] at cc ⊢
simp only [coe_map, card_map]
exact ⟨cc.left.of_induce, cc.right⟩
