V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
C : ConnectedComponent G
φ : G →g G'
ψ : G' →g G''
⊢ ∀ (v : V), map ψ (map φ (connectedComponentMk G v)) = map (Hom.comp ψ φ) (connectedComponentMk G v)
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
C : ConnectedComponent G
φ : G →g G'
ψ : G' →g G''
⊢ map ψ (map φ C) = map (Hom.comp ψ φ) C
refine' C.ind _
no goals
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
C : ConnectedComponent G
φ : G →g G'
ψ : G' →g G''
⊢ ∀ (v : V), map ψ (map φ (connectedComponentMk G v)) = map (Hom.comp ψ φ) (connectedComponentMk G v)
exact fun _ => rfl