induce_mono_right

Mathlib.Combinatorics.SimpleGraph.Subgraph

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

English

If s ⊆ s' then G'.induce s ≤ G'.induce s'.

Русский

Если s ⊆ s', то G'.induce s ≤ G'.induce s'.

LaTeX

$$$ (hs:\\subseteq) \\Rightarrow G'.induce s ≤ G'.induce s' $$$

Lean4

@[mono]
theorem induce_mono_right (hs : s ⊆ s') : G'.induce s ≤ G'.induce s' :=
  induce_mono le_rfl hs

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

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

Разделы

Аффилиация

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