Decidable adjacency in a disjoint sum

[UPSTREAM] candidate for Mathlib/Combinatorics/SimpleGraph/Sum.lean: the adjacency of a disjoint sum of two graphs with decidable adjacency is decidable.

@[instance_reducible]

instance SimpleGraph.instDecidableRelSumAdjSum_linglib {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} [DecidableRel G.Adj] [DecidableRel H.Adj] : DecidableRel (G ⊕g H).Adj

Equations

• SimpleGraph.instDecidableRelSumAdjSum_linglib (Sum.inl val) (Sum.inl val_1) = decidable_of_iff' (G.Adj val val_1) ⋯
• SimpleGraph.instDecidableRelSumAdjSum_linglib (Sum.inr val) (Sum.inr val_1) = decidable_of_iff' (H.Adj val val_1) ⋯
• SimpleGraph.instDecidableRelSumAdjSum_linglib (Sum.inl val) (Sum.inr val_1) = isFalse ⋯
• SimpleGraph.instDecidableRelSumAdjSum_linglib (Sum.inr val) (Sum.inl val_1) = isFalse ⋯