cliqueFinset_map — Mathlib

English

Under an embedding f, the n-cliques of G map to n-cliques of G.map f.

Русский

При отображении f клики n отображаются в клики n графа G.map f.

LaTeX

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

Lean4

@[simp]
theorem cliqueFinset_map (f : α ↪ β) (hn : n ≠ 1) :
    (G.map f).cliqueFinset n = (G.cliqueFinset n).map ⟨map f, Finset.map_injective _⟩ :=
  coe_injective <| by simp_rw [coe_cliqueFinset, cliqueSet_map hn, coe_map, coe_cliqueFinset, Embedding.coeFn_mk]

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