English
The disjoint sum G ⊕ H is a graph on α ⊕ β whose adjacency is given by G.Adj on the left side, H.Adj on the right side, and false across the two sides.
Русский
Дизъюнктное сложение G ⊕ H — граф на декомпозиции α ⊕ β, где смежность внутри каждого компонента сохраняется, а между компонентами нет связей.
LaTeX
$$$\\text{SimpleGraph.sum}(G,H) : \\text{SimpleGraph}(α \\oplus β)$ with Adj(u,v) = G.Adj if u,v ∈ α, H.Adj if u,v ∈ β, and false otherwise$$
Lean4
/-- Disjoint sum of `G` and `H`. -/
@[simps!]
protected def sum (G : SimpleGraph α) (H : SimpleGraph β) : SimpleGraph (α ⊕ β)
where
Adj
| Sum.inl u, Sum.inl v => G.Adj u v
| Sum.inr u, Sum.inr v => H.Adj u v
| _, _ => false
symm
| Sum.inl u, Sum.inl v => G.adj_symm
| Sum.inr u, Sum.inr v => H.adj_symm
| Sum.inl _, Sum.inr _ | Sum.inr _, Sum.inl _ => id
loopless u := by cases u <;> simp
