α : Type u
β : Type v
γ : Type ?u.11276
inst✝² : OmegaCompletePartialOrder α
inst✝¹ : OmegaCompletePartialOrder β
inst✝ : OmegaCompletePartialOrder γ
f : α →o β
g : β →o γ
c : Chain α
⊢ ↑OrderHom.id (ωSup c) = ωSup (map c OrderHom.id)
α : Type u
β : Type v
γ : Type ?u.11276
inst✝² : OmegaCompletePartialOrder α
inst✝¹ : OmegaCompletePartialOrder β
inst✝ : OmegaCompletePartialOrder γ
f : α →o β
g : β →o γ
⊢ Continuous OrderHom.id
intro c
α : Type u
β : Type v
γ : Type ?u.11276
inst✝² : OmegaCompletePartialOrder α
inst✝¹ : OmegaCompletePartialOrder β
inst✝ : OmegaCompletePartialOrder γ
f : α →o β
g : β →o γ
c : Chain α
⊢ ↑OrderHom.id (ωSup c) = ωSup c
α : Type u
β : Type v
γ : Type ?u.11276
inst✝² : OmegaCompletePartialOrder α
inst✝¹ : OmegaCompletePartialOrder β
inst✝ : OmegaCompletePartialOrder γ
f : α →o β
g : β →o γ
c : Chain α
⊢ ↑OrderHom.id (ωSup c) = ωSup (map c OrderHom.id)
rw [c.map_id]
no goals
α : Type u
β : Type v
γ : Type ?u.11276
inst✝² : OmegaCompletePartialOrder α
inst✝¹ : OmegaCompletePartialOrder β
inst✝ : OmegaCompletePartialOrder γ
f : α →o β
g : β →o γ
c : Chain α
⊢ ↑OrderHom.id (ωSup c) = ωSup c
rfl