α : Type u_1
β : Type u_2
γ : Type ?u.82889
G : SimpleGraph α
H : SimpleGraph β
hG : Connected G
hH : Connected H
this : Nonempty α
⊢ Connected (G □ H)
α : Type u_1
β : Type u_2
γ : Type ?u.82889
G : SimpleGraph α
H : SimpleGraph β
hG : Connected G
hH : Connected H
⊢ Connected (G □ H)
haveI := hG.nonempty
α : Type u_1
β : Type u_2
γ : Type ?u.82889
G : SimpleGraph α
H : SimpleGraph β
hG : Connected G
hH : Connected H
this✝ : Nonempty α
this : Nonempty β
⊢ Connected (G □ H)
α : Type u_1
β : Type u_2
γ : Type ?u.82889
G : SimpleGraph α
H : SimpleGraph β
hG : Connected G
hH : Connected H
this : Nonempty α
⊢ Connected (G □ H)
haveI := hH.nonempty
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.82889
G : SimpleGraph α
H : SimpleGraph β
hG : Connected G
hH : Connected H
this✝ : Nonempty α
this : Nonempty β
⊢ Connected (G □ H)
exact ⟨hG.preconnected.boxProd hH.preconnected⟩