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

State before:
ι : Sort u_1
𝕜 : Type ?u.13166
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 [iInf]
State after:
no goals