ι : Sort ?u.208589
𝕜 : Type ?u.208592
V : Type u
W : Type v
X : Type w
G✝ : SimpleGraph V
G'✝ : SimpleGraph W
a b c u v w : V
e : Sym2 V
f : V ↪ W
G G' : SimpleGraph W
h : G ≤ G'
v✝ w✝ : V
ha : Adj (SimpleGraph.comap (↑f) G) v✝ w✝
⊢ Adj (SimpleGraph.comap (↑f) G') v✝ w✝
ι : Sort ?u.208589
𝕜 : Type ?u.208592
V : Type u
W : Type v
X : Type w
G : SimpleGraph V
G' : SimpleGraph W
a b c u v w : V
e : Sym2 V
f : V ↪ W
⊢ Monotone (SimpleGraph.comap ↑f)
intro G G' h _ _ ha
no goals
ι : Sort ?u.208589
𝕜 : Type ?u.208592
V : Type u
W : Type v
X : Type w
G✝ : SimpleGraph V
G'✝ : SimpleGraph W
a b c u v w : V
e : Sym2 V
f : V ↪ W
G G' : SimpleGraph W
h : G ≤ G'
v✝ w✝ : V
ha : Adj (SimpleGraph.comap (↑f) G) v✝ w✝
⊢ Adj (SimpleGraph.comap (↑f) G') v✝ w✝
exact h ha