hom_injective

Mathlib.Combinatorics.SimpleGraph.Subgraph

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

English

The subgraph homomorphism x.hom is injective for every subgraph x.

Русский

Гомоморфизм x.hom единичен по всем подграфам x.

LaTeX

$$$\forall x : \text{Subgraph}(G),\ \operatorname{Injective}(x.\mathrm{hom}).$$$

Lean4

theorem hom_injective {x : Subgraph G} : Function.Injective x.hom := fun _ _ ↦ Subtype.ext

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

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

Разделы

Аффилиация

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