ι : Sort ?u.100917
𝕜 : Type ?u.100920
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
h : Adj G a b
⊢ {Quotient.mk (Sym2.Rel.setoid V) (a, b)} ⊆ incidenceSet G a ∩ incidenceSet G b
ι : Sort ?u.100917
𝕜 : Type ?u.100920
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
h : Adj G a b
⊢ incidenceSet G a ∩ incidenceSet G b = {Quotient.mk (Sym2.Rel.setoid V) (a, b)}
refine' (G.incidenceSet_inter_incidenceSet_subset <| h.ne).antisymm _
ι : Sort ?u.100917
𝕜 : Type ?u.100920
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
h : Adj G a b
⊢ Quotient.mk (Sym2.Rel.setoid V) (a, b) ∈ incidenceSet G a ∩ incidenceSet G b
ι : Sort ?u.100917
𝕜 : Type ?u.100920
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
h : Adj G a b
⊢ {Quotient.mk (Sym2.Rel.setoid V) (a, b)} ⊆ incidenceSet G a ∩ incidenceSet G b
rintro _ (rfl : _ = ⟦(a, b)⟧)
no goals
ι : Sort ?u.100917
𝕜 : Type ?u.100920
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
h : Adj G a b
⊢ Quotient.mk (Sym2.Rel.setoid V) (a, b) ∈ incidenceSet G a ∩ incidenceSet G b
exact ⟨G.mk'_mem_incidenceSet_left_iff.2 h, G.mk'_mem_incidenceSet_right_iff.2 h⟩