Theorem: Digraph.iSup_adj (GraphProjects/Digraph.lean)

State before:
ι : Sort u_1
𝕜 : Type ?u.10671
V : Type u
W : Type v
X : Type w
G : Digraph V
G' : Digraph W
a b c u v w : V
f : ι → Digraph V
⊢ (⨆ (i : ι), f i).Adj a b ↔ ∃ i, (f i).Adj a b
Tactic:
simp [iSup]
State after:
no goals