α : Type u
β : Type v
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
c : Chain α
⊢ ↑⊤ (ωSup c) = ωSup (Chain.map c ⊤)
α : Type u
β : Type v
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
⊢ Continuous ⊤
intro c
case H
α : Type u
β : Type v
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
c : Chain α
⊢ ∀ (c_1 : β), ↑⊤ (ωSup c) ≤ c_1 ↔ ωSup (Chain.map c ⊤) ≤ c_1
α : Type u
β : Type v
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
c : Chain α
⊢ ↑⊤ (ωSup c) = ωSup (Chain.map c ⊤)
apply eq_of_forall_ge_iff
case H
α : Type u
β : Type v
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
c : Chain α
z : β
⊢ ↑⊤ (ωSup c) ≤ z ↔ ωSup (Chain.map c ⊤) ≤ z
case H
α : Type u
β : Type v
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
c : Chain α
⊢ ∀ (c_1 : β), ↑⊤ (ωSup c) ≤ c_1 ↔ ωSup (Chain.map c ⊤) ≤ c_1
intro z
no goals
case H
α : Type u
β : Type v
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
c : Chain α
z : β
⊢ ↑⊤ (ωSup c) ≤ z ↔ ωSup (Chain.map c ⊤) ≤ z
simp only [OrderHom.instTopOrderHom_top, OrderHom.const_coe_coe, Function.const, top_le_iff,
  ωSup_le_iff, Chain.map_coe, Function.comp, forall_const]