ι : Sort ?u.167405
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : SimpleGraph W
f : G →g G'
H H' : Subgraph G'
h : H ≤ H'
⊢ Subgraph.comap f H ≤ Subgraph.comap f H'
ι : Sort ?u.167405
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : SimpleGraph W
f : G →g G'
⊢ Monotone (Subgraph.comap f)
intro H H' h
case left
ι : Sort ?u.167405
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : SimpleGraph W
f : G →g G'
H H' : Subgraph G'
h : H ≤ H'
⊢ (Subgraph.comap f H).verts ⊆ (Subgraph.comap f H').verts

case right
ι : Sort ?u.167405
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : SimpleGraph W
f : G →g G'
H H' : Subgraph G'
h : H ≤ H'
⊢ ∀ ⦃v w : V⦄, Adj (Subgraph.comap f H) v w → Adj (Subgraph.comap f H') v w
ι : Sort ?u.167405
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : SimpleGraph W
f : G →g G'
H H' : Subgraph G'
h : H ≤ H'
⊢ Subgraph.comap f H ≤ Subgraph.comap f H'
constructor
case left
ι : Sort ?u.167405
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : SimpleGraph W
f : G →g G'
H H' : Subgraph G'
h : H ≤ H'
a✝ : V
⊢ a✝ ∈ (Subgraph.comap f H).verts → a✝ ∈ (Subgraph.comap f H').verts
case left
ι : Sort ?u.167405
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : SimpleGraph W
f : G →g G'
H H' : Subgraph G'
h : H ≤ H'
⊢ (Subgraph.comap f H).verts ⊆ (Subgraph.comap f H').verts
intro
case left
ι : Sort ?u.167405
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : SimpleGraph W
f : G →g G'
H H' : Subgraph G'
h : H ≤ H'
a✝ : V
⊢ ↑f a✝ ∈ H.verts → ↑f a✝ ∈ H'.verts
case left
ι : Sort ?u.167405
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : SimpleGraph W
f : G →g G'
H H' : Subgraph G'
h : H ≤ H'
a✝ : V
⊢ a✝ ∈ (Subgraph.comap f H).verts → a✝ ∈ (Subgraph.comap f H').verts
simp only [comap_verts, Set.mem_preimage]
no goals
case left
ι : Sort ?u.167405
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : SimpleGraph W
f : G →g G'
H H' : Subgraph G'
h : H ≤ H'
a✝ : V
⊢ ↑f a✝ ∈ H.verts → ↑f a✝ ∈ H'.verts
apply h.1
case right
ι : Sort ?u.167405
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : SimpleGraph W
f : G →g G'
H H' : Subgraph G'
h : H ≤ H'
v w : V
⊢ Adj (Subgraph.comap f H) v w → Adj (Subgraph.comap f H') v w
case right
ι : Sort ?u.167405
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : SimpleGraph W
f : G →g G'
H H' : Subgraph G'
h : H ≤ H'
⊢ ∀ ⦃v w : V⦄, Adj (Subgraph.comap f H) v w → Adj (Subgraph.comap f H') v w
intro v w
case right
ι : Sort ?u.167405
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : SimpleGraph W
f : G →g G'
H H' : Subgraph G'
h : H ≤ H'
v w : V
⊢ SimpleGraph.Adj G v w → Adj H (↑f v) (↑f w) → Adj H' (↑f v) (↑f w)
case right
ι : Sort ?u.167405
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : SimpleGraph W
f : G →g G'
H H' : Subgraph G'
h : H ≤ H'
v w : V
⊢ Adj (Subgraph.comap f H) v w → Adj (Subgraph.comap f H') v w
simp (config := { contextual := true }) only [comap_Adj, and_imp, true_and_iff]
case right
ι : Sort ?u.167405
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : SimpleGraph W
f : G →g G'
H H' : Subgraph G'
h : H ≤ H'
v w : V
a✝ : SimpleGraph.Adj G v w
⊢ Adj H (↑f v) (↑f w) → Adj H' (↑f v) (↑f w)
case right
ι : Sort ?u.167405
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : SimpleGraph W
f : G →g G'
H H' : Subgraph G'
h : H ≤ H'
v w : V
⊢ SimpleGraph.Adj G v w → Adj H (↑f v) (↑f w) → Adj H' (↑f v) (↑f w)
intro
no goals
case right
ι : Sort ?u.167405
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
G' : SimpleGraph W
f : G →g G'
H H' : Subgraph G'
h : H ≤ H'
v w : V
a✝ : SimpleGraph.Adj G v w
⊢ Adj H (↑f v) (↑f w) → Adj H' (↑f v) (↑f w)
apply h.2