ι : Sort ?u.145982
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.map f H ≤ Subgraph.map f H'
ι : Sort ?u.145982
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.map f)
intro H H' h
case left
ι : Sort ?u.145982
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.map f H).verts ⊆ (Subgraph.map f H').verts

case right
ι : Sort ?u.145982
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 : W⦄, Adj (Subgraph.map f H) v w → Adj (Subgraph.map f H') v w
ι : Sort ?u.145982
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.map f H ≤ Subgraph.map f H'
constructor
case left
ι : Sort ?u.145982
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✝ : W
⊢ a✝ ∈ (Subgraph.map f H).verts → a✝ ∈ (Subgraph.map f H').verts
case left
ι : Sort ?u.145982
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.map f H).verts ⊆ (Subgraph.map f H').verts
intro
case left
ι : Sort ?u.145982
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✝ : W
⊢ ∀ (x : V), x ∈ H.verts → ↑f x = a✝ → ∃ x, x ∈ H'.verts ∧ ↑f x = a✝
case left
ι : Sort ?u.145982
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✝ : W
⊢ a✝ ∈ (Subgraph.map f H).verts → a✝ ∈ (Subgraph.map f H').verts
simp only [map_verts, Set.mem_image, forall_exists_index, and_imp]
case left
ι : Sort ?u.145982
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 : V
hv : v ∈ H.verts
⊢ ∃ x, x ∈ H'.verts ∧ ↑f x = ↑f v
case left
ι : Sort ?u.145982
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✝ : W
⊢ ∀ (x : V), x ∈ H.verts → ↑f x = a✝ → ∃ x, x ∈ H'.verts ∧ ↑f x = a✝
rintro v hv rfl
no goals
case left
ι : Sort ?u.145982
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 : V
hv : v ∈ H.verts
⊢ ∃ x, x ∈ H'.verts ∧ ↑f x = ↑f v
exact ⟨_, h.1 hv, rfl⟩
case right.intro.intro.intro.intro
ι : Sort ?u.145982
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'
u v : V
ha : Adj H u v
⊢ Adj (Subgraph.map f H') (↑f u) (↑f v)
case right
ι : Sort ?u.145982
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 : W⦄, Adj (Subgraph.map f H) v w → Adj (Subgraph.map f H') v w
rintro _ _ ⟨u, v, ha, rfl, rfl⟩
no goals
case right.intro.intro.intro.intro
ι : Sort ?u.145982
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'
u v : V
ha : Adj H u v
⊢ Adj (Subgraph.map f H') (↑f u) (↑f v)
exact ⟨_, _, h.2 ha, rfl, rfl⟩