induceHomOfLE_apply

Mathlib.Combinatorics.SimpleGraph.Maps

URI: https://scilib.ai/kg/mathlib#SimpleGraph.induceHomOfLE_apply

English

For v ∈ s, the induced embedding on the restriction equals the inclusion of v into s'.

Русский

Для v ∈ s индуцированное вложение равно включению v в s'.

LaTeX

$$$ \forall v \in s,\ (G.induceHomOfLE h) v = \mathrm{Set.inclusion}(h) v$$$

Lean4

@[simp]
theorem induceHomOfLE_apply (v : s) : (G.induceHomOfLE h) v = Set.inclusion h v :=
  rfl

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

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

Разделы

Аффилиация

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