case mp
α : Type u
β : Type v
γ : Type ?u.8324
inst✝ : OmegaCompletePartialOrder α
c : Chain α
x : α
a✝ : ωSup c ≤ x
i✝ : ℕ
⊢ ↑c i✝ ≤ x

case mpr
α : Type u
β : Type v
γ : Type ?u.8324
inst✝ : OmegaCompletePartialOrder α
c : Chain α
x : α
a✝ : ∀ (i : ℕ), ↑c i ≤ x
⊢ ωSup c ≤ x
α : Type u
β : Type v
γ : Type ?u.8324
inst✝ : OmegaCompletePartialOrder α
c : Chain α
x : α
⊢ ωSup c ≤ x ↔ ∀ (i : ℕ), ↑c i ≤ x
constructor <;> intros
no goals
case mpr
α : Type u
β : Type v
γ : Type ?u.8324
inst✝ : OmegaCompletePartialOrder α
c : Chain α
x : α
a✝ : ∀ (i : ℕ), ↑c i ≤ x
⊢ ωSup c ≤ x
exact ωSup_le _ _ ‹_›
α : Type u
β : Type v
γ : Type ?u.8324
inst✝ : OmegaCompletePartialOrder α
c : Chain α
x : α
a✝ : ωSup c ≤ x
i✝ : ℕ
⊢ ↑c i✝ ≤ ωSup c

α : Type u
β : Type v
γ : Type ?u.8324
inst✝ : OmegaCompletePartialOrder α
c : Chain α
x : α
a✝ : ωSup c ≤ x
i✝ : ℕ
⊢ ωSup c ≤ x
case mp
α : Type u
β : Type v
γ : Type ?u.8324
inst✝ : OmegaCompletePartialOrder α
c : Chain α
x : α
a✝ : ωSup c ≤ x
i✝ : ℕ
⊢ ↑c i✝ ≤ x
trans ωSup c
α : Type u
β : Type v
γ : Type ?u.8324
inst✝ : OmegaCompletePartialOrder α
c : Chain α
x : α
a✝ : ωSup c ≤ x
i✝ : ℕ
⊢ ωSup c ≤ x
α : Type u
β : Type v
γ : Type ?u.8324
inst✝ : OmegaCompletePartialOrder α
c : Chain α
x : α
a✝ : ωSup c ≤ x
i✝ : ℕ
⊢ ↑c i✝ ≤ ωSup c

α : Type u
β : Type v
γ : Type ?u.8324
inst✝ : OmegaCompletePartialOrder α
c : Chain α
x : α
a✝ : ωSup c ≤ x
i✝ : ℕ
⊢ ωSup c ≤ x
exact le_ωSup _ _
no goals
α : Type u
β : Type v
γ : Type ?u.8324
inst✝ : OmegaCompletePartialOrder α
c : Chain α
x : α
a✝ : ωSup c ≤ x
i✝ : ℕ
⊢ ωSup c ≤ x
assumption