mono

Mathlib.Combinatorics.SimpleGraph.Clique

URI: https://scilib.ai/kg/mathlib#SimpleGraph.IsClique.mono

English

If G ≤ H and s is a clique in G, then s is a clique in H.

Русский

Если G ≤ H и s является кликой в G, то s является кликой в H.

LaTeX

$$$ h : G \le H \rightarrow G.IsClique s \rightarrow H.IsClique s $$$

Lean4

theorem mono (h : G ≤ H) : G.IsClique s → H.IsClique s :=
  Set.Pairwise.mono' h

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru