isContained

Mathlib.Combinatorics.SimpleGraph.Copy

URI: https://scilib.ai/kg/mathlib#SimpleGraph.IsIndContained.isContained

English

From an induced containment relation we obtain a standard containment relation: existence of an embedding implies inclusion.

Русский

Из отношения индуцированного вложения следует обычное включение: существование вложения приводит к включению.

LaTeX

$$G ⊴ H → G ⊑ H$$

Lean4

protected theorem isContained : G ⊴ H → G ⊑ H := fun ⟨f⟩ ↦ ⟨f.toCopy⟩

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

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

Разделы

Аффилиация

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