subset

Mathlib.Combinatorics.SimpleGraph.Clique

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

English

If t ⊆ s and G.IsClique s, then G.IsClique t.

Русский

Если t ⊆ s и G.IsClique s, то G.IsClique t.

LaTeX

$$$ h : t \subseteq s \rightarrow G.IsClique s \rightarrow G.IsClique t $$$

Lean4

theorem subset (h : t ⊆ s) : G.IsClique s → G.IsClique t :=
  Set.Pairwise.mono h

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

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

Разделы

Аффилиация

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