case h
ι : Sort ?u.90110
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
s : Set (Subgraph G)
v x✝ : V
⊢ x✝ ∈ neighborSet (sSup s) v ↔ x✝ ∈ ⋃ (G' : Subgraph G) (_ : G' ∈ s), neighborSet G' v
ι : Sort ?u.90110
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
s : Set (Subgraph G)
v : V
⊢ neighborSet (sSup s) v = ⋃ (G' : Subgraph G) (_ : G' ∈ s), neighborSet G' v
ext
no goals
case h
ι : Sort ?u.90110
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
s : Set (Subgraph G)
v x✝ : V
⊢ x✝ ∈ neighborSet (sSup s) v ↔ x✝ ∈ ⋃ (G' : Subgraph G) (_ : G' ∈ s), neighborSet G' v
simp