V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
hconn : Preconnected G
u v : V
⊢ Nonempty (Walk G u v)
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
hconn : Preconnected G
u v : V
⊢ Set.Nonempty Set.univ
rw [← Set.nonempty_iff_univ_nonempty]
no goals
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
hconn : Preconnected G
u v : V
⊢ Nonempty (Walk G u v)
exact hconn u v