induce_mono_left

Mathlib.Combinatorics.SimpleGraph.Subgraph

URI: https://scilib.ai/kg/mathlib#SimpleGraph.Subgraph.induce_mono_left

English

If G' ≤ G'' then G'.induce s ≤ G''.induce s for any s.

Русский

Если G' ≤ G'', то для любого s выполняется G'.induce s ≤ G''.induce s.

LaTeX

$$$ (hg:\\le) \\Rightarrow G'.induce s ≤ G''.induce s $$$

Lean4

@[mono]
theorem induce_mono_left (hg : G' ≤ G'') : G'.induce s ≤ G''.induce s :=
  induce_mono hg subset_rfl

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

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

Разделы

Аффилиация

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