comap — Mathlib

English

If there is an embedding f: H ↪g G, then G.CliqueFree n implies H.CliqueFree n.

Русский

Если существует вложение f: H ↪g G, то из G.CliqueFree n следует H.CliqueFree n.

LaTeX

$$$ (f : H \hookrightarrow G) : G.CliqueFree(n) \Rightarrow H.CliqueFree(n). $$$

Lean4

/-- If a graph is cliquefree, any graph that embeds into it is also cliquefree. -/
theorem comap {H : SimpleGraph β} (f : H ↪g G) : G.CliqueFree n → H.CliqueFree n :=
  by
  intro h; contrapose h
  exact not_cliqueFree_of_top_embedding <| f.comp (topEmbeddingOfNotCliqueFree h)

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