sumInl — Mathlib

English

The embedding of G into G ⊕g H preserves adjacencies: (Sum.inl u) is adjacent to (Sum.inl v) in the sum graph exactly when u is adjacent to v in G.

Русский

Встраивание G в G ⊕g H сохраняет смежности: (Sum.inl u) смежен с (Sum.inl v) в суммированном графе тогда и только тогда, когда u смежен с v в G.

LaTeX

$$$\text{sumInl} : G \hookrightarrow_g (G \oplus_g H),\; (G \oplus_g H).Adj (Sum.inl\, u) (Sum.inl\, v) \iff G.Adj u v.$$$

Lean4

/-- The embedding of `G` into `G ⊕g H`. -/
@[simps]
def sumInl : G ↪g G ⊕g H where
  toFun u := _root_.Sum.inl u
  inj' u v := by simp
  map_rel_iff' := by simp

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