sumInr — Mathlib

English

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

Русский

Встраивание H в G ⊕g H сохраняет смежности: (Sum.inr a) смежен с (Sum.inr b) тогда и только тогда, когда a смежен с b в H.

LaTeX

$$$\text{sumInr} : H \hookrightarrow_g (G \oplus_g H),\; (G \oplus_g H).Adj (Sum.inr\, a) (Sum.inr\, b) \iff H.Adj a b.$$$

Lean4

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

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