ofLE

Mathlib.Combinatorics.SimpleGraph.Maps

URI: https://scilib.ai/kg/mathlib#SimpleGraph.Hom.ofLE

Lean4

/-- The graph homomorphism from a smaller graph to a bigger one. -/
def ofLE (h : G₁ ≤ G₂) : G₁ →g G₂ :=
  ⟨id, @h⟩

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

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

Разделы

Аффилиация

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