topEmbeddingOfNotCliqueFree — Mathlib

English

There exists a top embedding witnessing not_cliqueFree_iff; i.e., a top embedding into G certifies not being clique-free.

Русский

Существует топ-встраивание, подтверждающее, что не clique-free; то есть существование вложения вершины из полного графа в G доказывает несвободность клики.

LaTeX

$$$ \exists f : (\top : SimpleGraph(Fin n)) \hookrightarrow G, \text{ witness of not_cliqueFree}. $$$

Lean4

/-- An embedding of a complete graph that witnesses the fact that the graph is not clique-free. -/
noncomputable def topEmbeddingOfNotCliqueFree {n : ℕ} (h : ¬G.CliqueFree n) : (⊤ : SimpleGraph (Fin n)) ↪g G :=
  by
  simp only [CliqueFree, isNClique_iff, isClique_iff_induce_eq, not_forall, Classical.not_not] at h
  obtain ⟨ha, hb⟩ := h.choose_spec
  have : (⊤ : SimpleGraph (Fin #h.choose)) ≃g (⊤ : SimpleGraph h.choose) :=
    by
    apply Iso.completeGraph
    simpa using (Fintype.equivFin h.choose).symm
  rw [← ha] at this
  convert (Embedding.induce ↑h.choose.toSet).comp this.toEmbedding
  exact hb.symm

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