cliqueSet_map_of_equiv — Mathlib

English

If there is a bijection between vertex sets, the cliqueSet is transported accordingly.

Русский

Если существует биекция между множества вершин, то cliqueSet переносится соответствующим образом.

LaTeX

$$For an equivalence $e$, $(G.map e).cliqueSet(n) = \operatorname{image}(\operatorname{Finset.map}(e))(G.cliqueSet(n))$.$$

Lean4

@[simp]
theorem cliqueSet_map_of_equiv (G : SimpleGraph α) (e : α ≃ β) (n : ℕ) :
    (G.map e.toEmbedding).cliqueSet n = map e.toEmbedding '' G.cliqueSet n :=
  by
  obtain rfl | hn := eq_or_ne n 1
  · ext
    simp [e.exists_congr_left]
  · exact cliqueSet_map hn _ _

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