English
If A is a clique in the subgraph induced by a superset F, then the embedding of A into G (i.e., Subtype.val '' A) is a clique in G.
Русский
Если A образует клику в подграфе, индуцированном над множеством F, то встроение A в G является кликой в G.
LaTeX
$$$$\\text{If } A \\subseteq F \\text{ is a clique in } (S.induce F).coe, \\text{ then } G.IsClique(\\text{Subtype.val }'' A).$$$$
Lean4
/-- If a set of vertices `A` is a clique in subgraph of `G` induced by a superset of `A`,
its embedding is a clique in `G`. -/
theorem of_induce {S : Subgraph G} {F : Set α} {A : Set F} (c : (S.induce F).coe.IsClique A) :
G.IsClique (Subtype.val '' A) :=
by
simp only [Set.Pairwise, Set.mem_image, Subtype.exists, exists_and_right, exists_eq_right]
intro _ ⟨_, ainA⟩ _ ⟨_, binA⟩ anb
exact S.adj_sub (c ainA binA (Subtype.coe_ne_coe.mp anb)).2.2
