α : Type u
β : Type v
γ : Type ?u.12251
inst✝² : OmegaCompletePartialOrder α
inst✝¹ : OmegaCompletePartialOrder β
inst✝ : OmegaCompletePartialOrder γ
f : α →o β
g : β →o γ
x : β
c : Chain α
z : β
⊢ Function.const α x (ωSup c) ≤ z ↔ ∀ (i : ℕ), (Function.const α x ∘ ↑c) i ≤ z
α : Type u
β : Type v
γ : Type ?u.12251
inst✝² : OmegaCompletePartialOrder α
inst✝¹ : OmegaCompletePartialOrder β
inst✝ : OmegaCompletePartialOrder γ
f : α →o β
g : β →o γ
x : β
c : Chain α
z : β
⊢ ↑(↑(OrderHom.const α) x) (ωSup c) ≤ z ↔ ωSup (map c (↑(OrderHom.const α) x)) ≤ z
rw [ωSup_le_iff, Chain.map_coe, OrderHom.const_coe_coe]
no goals
α : Type u
β : Type v
γ : Type ?u.12251
inst✝² : OmegaCompletePartialOrder α
inst✝¹ : OmegaCompletePartialOrder β
inst✝ : OmegaCompletePartialOrder γ
f : α →o β
g : β →o γ
x : β
c : Chain α
z : β
⊢ Function.const α x (ωSup c) ≤ z ↔ ∀ (i : ℕ), (Function.const α x ∘ ↑c) i ≤ z
simp