case h
ι : Sort ?u.112949
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
s : Set (Subgraph G)
e : Sym2 V
⊢ e ∈ edgeSet (sInf s) ↔ e ∈ (⋂ (G' : Subgraph G) (_ : G' ∈ s), edgeSet G') ∩ SimpleGraph.edgeSet G
ι : Sort ?u.112949
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
s : Set (Subgraph G)
⊢ edgeSet (sInf s) = (⋂ (G' : Subgraph G) (_ : G' ∈ s), edgeSet G') ∩ SimpleGraph.edgeSet G
ext e
case h.h
ι : Sort ?u.112949
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
s : Set (Subgraph G)
x✝ y✝ : V
⊢ Quotient.mk (Sym2.Rel.setoid V) (x✝, y✝) ∈ edgeSet (sInf s) ↔
    Quotient.mk (Sym2.Rel.setoid V) (x✝, y✝) ∈ (⋂ (G' : Subgraph G) (_ : G' ∈ s), edgeSet G') ∩ SimpleGraph.edgeSet G
case h
ι : Sort ?u.112949
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
s : Set (Subgraph G)
e : Sym2 V
⊢ e ∈ edgeSet (sInf s) ↔ e ∈ (⋂ (G' : Subgraph G) (_ : G' ∈ s), edgeSet G') ∩ SimpleGraph.edgeSet G
induction e using Sym2.ind
no goals
case h.h
ι : Sort ?u.112949
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
s : Set (Subgraph G)
x✝ y✝ : V
⊢ Quotient.mk (Sym2.Rel.setoid V) (x✝, y✝) ∈ edgeSet (sInf s) ↔
    Quotient.mk (Sym2.Rel.setoid V) (x✝, y✝) ∈ (⋂ (G' : Subgraph G) (_ : G' ∈ s), edgeSet G') ∩ SimpleGraph.edgeSet G
simp