injective

Mathlib.Combinatorics.SimpleGraph.Subgraph

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

← MathLib Explorer

English

If x ≤ y, then the inclusion map from x to y is injective.

Русский

Если x ⊆ y, то включение x в y инъективно.

LaTeX

$$$\forall x,y : \text{Subgraph}(G),\ x \le y \Rightarrow \operatorname{Injective}(\text{inclusion}(h)).$$$

Lean4

theorem injective {x y : Subgraph G} (h : x ≤ y) : Function.Injective (inclusion h) :=
  by
  intro v w h
  rw [inclusion, DFunLike.coe, Subtype.mk_eq_mk] at h
  exact Subtype.ext h

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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