case h.mk.mk
ι : Sort ?u.70630
𝕜 : Type ?u.70633
V : Type u
W : Type v
X : Type w
G : SimpleGraph V
G' : SimpleGraph W
a b c u v w : V
e : Sym2 V
G₁ G₂ : SimpleGraph V
x✝ : Sym2 V
x y : V
⊢ Quot.mk Setoid.r (x, y) ∈ edgeSet (G₁ ⊓ G₂) ↔ Quot.mk Setoid.r (x, y) ∈ edgeSet G₁ ∩ edgeSet G₂
ι : Sort ?u.70630
𝕜 : Type ?u.70633
V : Type u
W : Type v
X : Type w
G : SimpleGraph V
G' : SimpleGraph W
a b c u v w : V
e : Sym2 V
G₁ G₂ : SimpleGraph V
⊢ edgeSet (G₁ ⊓ G₂) = edgeSet G₁ ∩ edgeSet G₂
ext ⟨x, y⟩
no goals
case h.mk.mk
ι : Sort ?u.70630
𝕜 : Type ?u.70633
V : Type u
W : Type v
X : Type w
G : SimpleGraph V
G' : SimpleGraph W
a b c u v w : V
e : Sym2 V
G₁ G₂ : SimpleGraph V
x✝ : Sym2 V
x y : V
⊢ Quot.mk Setoid.r (x, y) ∈ edgeSet (G₁ ⊓ G₂) ↔ Quot.mk Setoid.r (x, y) ∈ edgeSet G₁ ∩ edgeSet G₂
rfl