comap — Mathlib

English

If H embeds into G and G is complete multipartite, then H is also complete multipartite.

Русский

Если граф H вложен в граф G и G является полным мультитипным, то и H является полным мультитипным графом.

LaTeX

$$∀ f:(H ↪g G), G.IsCompleteMultipartite → H.IsCompleteMultipartite$$

Lean4

theorem comap {β : Type*} {H : SimpleGraph β} (f : H ↪g G) : G.IsCompleteMultipartite → H.IsCompleteMultipartite :=
  by
  intro h; contrapose h
  exact not_isCompleteMultipartite_of_pathGraph3ComplEmbedding <| f.comp (pathGraph3ComplEmbeddingOf h)

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