ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
inst✝ : Nonempty ι
f : ι → Subgraph G
⊢ (∀ (G' : Subgraph G), (G' ∈ Set.range fun i => f i) → Adj G' a b) ↔ ∀ (i : ι), Adj (f i) a b
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
inst✝ : Nonempty ι
f : ι → Subgraph G
⊢ Adj (⨅ (i : ι), f i) a b ↔ ∀ (i : ι), Adj (f i) a b
rw [iInf, sInf_adj_of_nonempty (Set.range_nonempty _)]
no goals
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
inst✝ : Nonempty ι
f : ι → Subgraph G
⊢ (∀ (G' : Subgraph G), (G' ∈ Set.range fun i => f i) → Adj G' a b) ↔ ∀ (i : ι), Adj (f i) a b
simp