case mp
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v : V
⊢ Reachable G u v → Relation.ReflTransGen G.Adj u v

case mpr
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v : V
⊢ Relation.ReflTransGen G.Adj u v → Reachable G u v
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v : V
⊢ Reachable G u v ↔ Relation.ReflTransGen G.Adj u v
constructor
case mp.intro
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v : V
h : Walk G u v
⊢ Relation.ReflTransGen G.Adj u v
case mp
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v : V
⊢ Reachable G u v → Relation.ReflTransGen G.Adj u v
rintro ⟨h⟩
no goals
case mp.intro
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v : V
h : Walk G u v
⊢ Relation.ReflTransGen G.Adj u v
induction h with
| nil => rfl
| cons h' _ ih => exact (Relation.ReflTransGen.single h').trans ih
no goals
case mp.intro.nil
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v u✝ : V
⊢ Relation.ReflTransGen G.Adj u✝ u✝
rfl
no goals
case mp.intro.cons
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v u✝ v✝ w✝ : V
h' : Adj G u✝ v✝
p✝ : Walk G v✝ w✝
ih : Relation.ReflTransGen G.Adj v✝ w✝
⊢ Relation.ReflTransGen G.Adj u✝ w✝
exact (Relation.ReflTransGen.single h').trans ih
case mpr
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v : V
h : Relation.ReflTransGen G.Adj u v
⊢ Reachable G u v
case mpr
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v : V
⊢ Relation.ReflTransGen G.Adj u v → Reachable G u v
intro h
no goals
case mpr
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v : V
h : Relation.ReflTransGen G.Adj u v
⊢ Reachable G u v
induction h with
| refl => rfl
| tail _ ha hr => exact Reachable.trans hr ⟨Walk.cons ha Walk.nil⟩
no goals
case mpr.refl
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v : V
⊢ Reachable G u u
rfl
no goals
case mpr.tail
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v b✝ c✝ : V
a✝ : Relation.ReflTransGen G.Adj u b✝
ha : Adj G b✝ c✝
hr : Reachable G u b✝
⊢ Reachable G u c✝
exact Reachable.trans hr ⟨Walk.cons ha Walk.nil⟩