cliqueFinset_map_of_equiv — Mathlib

English

Under an equivalence e, the n-cliques correspond under mapping.

Русский

При эквиваленции e n-клики соответствуют под действием отображения.

LaTeX

$$$(G.map e.toEmbedding).cliqueFinset n = (G.cliqueFinset n).map \\langle map e.toEmbedding, Finset.map_injective _\\rangle.$$$

Lean4

@[simp]
theorem cliqueFinset_map_of_equiv (e : α ≃ β) (n : ℕ) :
    (G.map e.toEmbedding).cliqueFinset n = (G.cliqueFinset n).map ⟨map e.toEmbedding, Finset.map_injective _⟩ :=
  coe_injective <| by push_cast; exact cliqueSet_map_of_equiv _ _ _

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