Decidable adjacency in a box product #
[UPSTREAM] candidate for Mathlib/Combinatorics/SimpleGraph/Prod.lean: the adjacency of a box
product of two graphs with decidable adjacency and decidable vertex equality is decidable.
@[instance_reducible]
instance
SimpleGraph.instDecidableRelProdAdjBoxProdOfDecidableEq_linglib
{α : Type u_1}
{β : Type u_2}
{G : SimpleGraph α}
{H : SimpleGraph β}
[DecidableEq α]
[DecidableEq β]
[DecidableRel G.Adj]
[DecidableRel H.Adj]
:
DecidableRel (G □ H).Adj
Equations
- SimpleGraph.instDecidableRelProdAdjBoxProdOfDecidableEq_linglib x✝¹ x✝ = decidable_of_iff' (G.Adj x✝¹.1 x✝.1 ∧ x✝¹.2 = x✝.2 ∨ H.Adj x✝¹.2 x✝.2 ∧ x✝¹.1 = x✝.1) ⋯