case left
ι : Sort ?u.258280
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : Subgraph G
s s' : Set V
hg : G' ≤ G''
hs : s ⊆ s'
⊢ (induce G' s).verts ⊆ (induce G'' s').verts

case right
ι : Sort ?u.258280
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : Subgraph G
s s' : Set V
hg : G' ≤ G''
hs : s ⊆ s'
⊢ ∀ ⦃v w : V⦄, Adj (induce G' s) v w → Adj (induce G'' s') v w
ι : Sort ?u.258280
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : Subgraph G
s s' : Set V
hg : G' ≤ G''
hs : s ⊆ s'
⊢ induce G' s ≤ induce G'' s'
constructor
no goals
case left
ι : Sort ?u.258280
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : Subgraph G
s s' : Set V
hg : G' ≤ G''
hs : s ⊆ s'
⊢ (induce G' s).verts ⊆ (induce G'' s').verts
simp [hs]
case right
ι : Sort ?u.258280
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : Subgraph G
s s' : Set V
hg : G' ≤ G''
hs : s ⊆ s'
⊢ ∀ ⦃v w : V⦄, v ∈ s → w ∈ s → Adj G' v w → v ∈ s' ∧ w ∈ s' ∧ Adj G'' v w
case right
ι : Sort ?u.258280
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : Subgraph G
s s' : Set V
hg : G' ≤ G''
hs : s ⊆ s'
⊢ ∀ ⦃v w : V⦄, Adj (induce G' s) v w → Adj (induce G'' s') v w
simp (config := { contextual := true }) only [induce_Adj, true_and_iff, and_imp]
case right
ι : Sort ?u.258280
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : Subgraph G
s s' : Set V
hg : G' ≤ G''
hs : s ⊆ s'
v w : V
hv : v ∈ s
hw : w ∈ s
ha : Adj G' v w
⊢ v ∈ s' ∧ w ∈ s' ∧ Adj G'' v w
case right
ι : Sort ?u.258280
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : Subgraph G
s s' : Set V
hg : G' ≤ G''
hs : s ⊆ s'
⊢ ∀ ⦃v w : V⦄, v ∈ s → w ∈ s → Adj G' v w → v ∈ s' ∧ w ∈ s' ∧ Adj G'' v w
intro v w hv hw ha
no goals
case right
ι : Sort ?u.258280
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : Subgraph G
s s' : Set V
hg : G' ≤ G''
hs : s ⊆ s'
v w : V
hv : v ∈ s
hw : w ∈ s
ha : Adj G' v w
⊢ v ∈ s' ∧ w ∈ s' ∧ Adj G'' v w
exact ⟨hs hv, hs hw, hg.2 ha⟩