isClique_range_copy_top — Mathlib

English

The vertices coming from a copy of the top element in a graph form a clique in the original graph.

Русский

Вершины, полученные копированием верхнего элемента, образуют клику в исходном графе.

LaTeX

$$$$ \\forall f:\\ copy(⊤, G),\\ G.IsClique( Set.range\\, f) $$$$

Lean4

/-- The vertices in a copy of `⊤` are a clique. -/
theorem isClique_range_copy_top (f : Copy (⊤ : SimpleGraph β) G) : G.IsClique (Set.range f) :=
  by
  intro _ ⟨_, h⟩ _ ⟨_, h'⟩ nh
  rw [← h, ← Copy.topEmbedding_apply, ← h', ← Copy.topEmbedding_apply] at nh ⊢
  rwa [← f.topEmbedding.coe_toEmbedding, (f.topEmbedding.apply_eq_iff_eq _ _).ne, ← top_adj, ←
    f.topEmbedding.map_adj_iff] at nh

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