case left
α : Type u_1
inst✝ : OmegaCompletePartialOrder α
c : Chain α
⊢ ∀ (i : ℕ), ↑c i ≤ ωSup c

case right
α : Type u_1
inst✝ : OmegaCompletePartialOrder α
c : Chain α
⊢ ∀ (y : α), (∀ (i : ℕ), ↑c i ≤ y) → ωSup c ≤ y
α : Type u_1
inst✝ : OmegaCompletePartialOrder α
c : Chain α
⊢ IsωSup c (ωSup c)
constructor
no goals
case left
α : Type u_1
inst✝ : OmegaCompletePartialOrder α
c : Chain α
⊢ ∀ (i : ℕ), ↑c i ≤ ωSup c
apply le_ωSup
no goals
case right
α : Type u_1
inst✝ : OmegaCompletePartialOrder α
c : Chain α
⊢ ∀ (y : α), (∀ (i : ℕ), ↑c i ≤ y) → ωSup c ≤ y
apply ωSup_le