case preconnected
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v w : V
hvw : Adj G v w
⊢ Preconnected (Subgraph.coe (subgraphOfAdj G hvw))
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v w : V
hvw : Adj G v w
⊢ Subgraph.Connected (subgraphOfAdj G hvw)
constructor
case preconnected.mk.mk
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v w : V
hvw : Adj G v w
a : V
ha : a ∈ (subgraphOfAdj G hvw).verts
b : V
hb : b ∈ (subgraphOfAdj G hvw).verts
⊢ Reachable (Subgraph.coe (subgraphOfAdj G hvw)) { val := a, property := ha } { val := b, property := hb }
case preconnected
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v w : V
hvw : Adj G v w
⊢ Preconnected (Subgraph.coe (subgraphOfAdj G hvw))
rintro ⟨a, ha⟩ ⟨b, hb⟩
case preconnected.mk.mk
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v w : V
hvw : Adj G v w
a : V
ha✝ : a ∈ (subgraphOfAdj G hvw).verts
b : V
hb✝ : b ∈ (subgraphOfAdj G hvw).verts
ha : a = v ∨ a = w
hb : b = v ∨ b = w
⊢ Reachable (Subgraph.coe (subgraphOfAdj G hvw)) { val := a, property := ha✝ } { val := b, property := hb✝ }
case preconnected.mk.mk
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v w : V
hvw : Adj G v w
a : V
ha : a ∈ (subgraphOfAdj G hvw).verts
b : V
hb : b ∈ (subgraphOfAdj G hvw).verts
⊢ Reachable (Subgraph.coe (subgraphOfAdj G hvw)) { val := a, property := ha } { val := b, property := hb }
simp only [subgraphOfAdj_verts, Set.mem_insert_iff, Set.mem_singleton_iff] at ha hb
no goals
case preconnected.mk.mk
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v w : V
hvw : Adj G v w
a : V
ha✝ : a ∈ (subgraphOfAdj G hvw).verts
b : V
hb✝ : b ∈ (subgraphOfAdj G hvw).verts
ha : a = v ∨ a = w
hb : b = v ∨ b = w
⊢ Reachable (Subgraph.coe (subgraphOfAdj G hvw)) { val := a, property := ha✝ } { val := b, property := hb✝ }
obtain rfl | rfl := ha <;> obtain rfl | rfl := hb <;>
  first | rfl | (apply Adj.reachable; simp)
no goals
case preconnected.mk.mk.inr.inr
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v b : V
hvw : Adj G v b
ha hb : b ∈ (subgraphOfAdj G hvw).verts
⊢ Reachable (Subgraph.coe (subgraphOfAdj G hvw)) { val := b, property := ha } { val := b, property := hb }
rfl
no goals
case preconnected.mk.mk.inr.inl
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
a b : V
hvw : Adj G b a
ha : a ∈ (subgraphOfAdj G hvw).verts
hb : b ∈ (subgraphOfAdj G hvw).verts
⊢ Reachable (Subgraph.coe (subgraphOfAdj G hvw)) { val := a, property := ha } { val := b, property := hb }
(apply Adj.reachable; simp)
case preconnected.mk.mk.inr.inl.h
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
a b : V
hvw : Adj G b a
ha : a ∈ (subgraphOfAdj G hvw).verts
hb : b ∈ (subgraphOfAdj G hvw).verts
⊢ Adj (Subgraph.coe (subgraphOfAdj G hvw)) { val := a, property := ha } { val := b, property := hb }
case preconnected.mk.mk.inr.inl
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
a b : V
hvw : Adj G b a
ha : a ∈ (subgraphOfAdj G hvw).verts
hb : b ∈ (subgraphOfAdj G hvw).verts
⊢ Reachable (Subgraph.coe (subgraphOfAdj G hvw)) { val := a, property := ha } { val := b, property := hb }
apply Adj.reachable
no goals
case preconnected.mk.mk.inr.inl.h
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
a b : V
hvw : Adj G b a
ha : a ∈ (subgraphOfAdj G hvw).verts
hb : b ∈ (subgraphOfAdj G hvw).verts
⊢ Adj (Subgraph.coe (subgraphOfAdj G hvw)) { val := a, property := ha } { val := b, property := hb }
simp