α : Type u
β : Type v
γ : Type ?u.4453
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
c c' : Chain α
f : α →o β
g✝ : β →o γ
g : α →o β
h : f ≤ g
i : ℕ
⊢ ∃ j, ↑f (↑c i) ≤ ↑g (↑c j)
α : Type u
β : Type v
γ : Type ?u.4453
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
c c' : Chain α
f : α →o β
g✝ : β →o γ
g : α →o β
h : f ≤ g
i : ℕ
⊢ ∃ j, ↑(map c f) i ≤ ↑(map c g) j
simp [mem_map_iff]
α : Type u
β : Type v
γ : Type ?u.4453
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
c c' : Chain α
f : α →o β
g✝ : β →o γ
g : α →o β
h : f ≤ g
i : ℕ
⊢ ∃ j, ↑f (↑c i) ≤ ↑g (↑c j)
α : Type u
β : Type v
γ : Type ?u.4453
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
c c' : Chain α
f : α →o β
g✝ : β →o γ
g : α →o β
h : f ≤ g
i : ℕ
⊢ ∃ j, ↑f (↑c i) ≤ ↑g (↑c j)
intros
α : Type u
β : Type v
γ : Type ?u.4453
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
c c' : Chain α
f : α →o β
g✝ : β →o γ
g : α →o β
h : f ≤ g
i : ℕ
⊢ ↑f (↑c i) ≤ ↑g (↑c i)
α : Type u
β : Type v
γ : Type ?u.4453
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
c c' : Chain α
f : α →o β
g✝ : β →o γ
g : α →o β
h : f ≤ g
i : ℕ
⊢ ∃ j, ↑f (↑c i) ≤ ↑g (↑c j)
exists i
no goals
α : Type u
β : Type v
γ : Type ?u.4453
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
c c' : Chain α
f : α →o β
g✝ : β →o γ
g : α →o β
h : f ≤ g
i : ℕ
⊢ ↑f (↑c i) ≤ ↑g (↑c i)
apply h