α : Type u_1
inst✝ : OmegaCompletePartialOrder α
y : Scott α
h : Monotone (notBelow y)
⊢ IsOpen (notBelow y)
α : Type u_1
inst✝ : OmegaCompletePartialOrder α
y : Scott α
⊢ IsOpen (notBelow y)
have h : Monotone (notBelow y) := by
  intro x y' h
  simp only [notBelow, setOf, le_Prop_eq]
  intro h₀ h₁
  apply h₀ (le_trans h h₁)
α : Type u_1
inst✝ : OmegaCompletePartialOrder α
y : Scott α
h : Monotone (notBelow y)
⊢ OmegaCompletePartialOrder.Continuous { toFun := fun x => x ∈ notBelow y, monotone' := h }
α : Type u_1
inst✝ : OmegaCompletePartialOrder α
y : Scott α
h : Monotone (notBelow y)
⊢ IsOpen (notBelow y)
exists h
α : Type u_1
inst✝ : OmegaCompletePartialOrder α
y : Scott α
h : Monotone (notBelow y)
c : Chain α
⊢ ↑{ toFun := fun x => x ∈ notBelow y, monotone' := h } (ωSup c) =
    ωSup (Chain.map c { toFun := fun x => x ∈ notBelow y, monotone' := h })
α : Type u_1
inst✝ : OmegaCompletePartialOrder α
y : Scott α
h : Monotone (notBelow y)
⊢ OmegaCompletePartialOrder.Continuous { toFun := fun x => x ∈ notBelow y, monotone' := h }
rintro c
case H
α : Type u_1
inst✝ : OmegaCompletePartialOrder α
y : Scott α
h : Monotone (notBelow y)
c : Chain α
⊢ ∀ (c_1 : Prop),
    ↑{ toFun := fun x => x ∈ notBelow y, monotone' := h } (ωSup c) ≤ c_1 ↔
      ωSup (Chain.map c { toFun := fun x => x ∈ notBelow y, monotone' := h }) ≤ c_1
α : Type u_1
inst✝ : OmegaCompletePartialOrder α
y : Scott α
h : Monotone (notBelow y)
c : Chain α
⊢ ↑{ toFun := fun x => x ∈ notBelow y, monotone' := h } (ωSup c) =
    ωSup (Chain.map c { toFun := fun x => x ∈ notBelow y, monotone' := h })
apply eq_of_forall_ge_iff
case H
α : Type u_1
inst✝ : OmegaCompletePartialOrder α
y : Scott α
h : Monotone (notBelow y)
c : Chain α
z : Prop
⊢ ↑{ toFun := fun x => x ∈ notBelow y, monotone' := h } (ωSup c) ≤ z ↔
    ωSup (Chain.map c { toFun := fun x => x ∈ notBelow y, monotone' := h }) ≤ z
case H
α : Type u_1
inst✝ : OmegaCompletePartialOrder α
y : Scott α
h : Monotone (notBelow y)
c : Chain α
⊢ ∀ (c_1 : Prop),
    ↑{ toFun := fun x => x ∈ notBelow y, monotone' := h } (ωSup c) ≤ c_1 ↔
      ωSup (Chain.map c { toFun := fun x => x ∈ notBelow y, monotone' := h }) ≤ c_1
intro z
case H
α : Type u_1
inst✝ : OmegaCompletePartialOrder α
y : Scott α
h : Monotone (notBelow y)
c : Chain α
z : Prop
⊢ ↑{ toFun := fun x => x ∈ notBelow y, monotone' := h } (ωSup c) ≤ z ↔
    ∀ (i : ℕ), ↑(Chain.map c { toFun := fun x => x ∈ notBelow y, monotone' := h }) i ≤ z
case H
α : Type u_1
inst✝ : OmegaCompletePartialOrder α
y : Scott α
h : Monotone (notBelow y)
c : Chain α
z : Prop
⊢ ↑{ toFun := fun x => x ∈ notBelow y, monotone' := h } (ωSup c) ≤ z ↔
    ωSup (Chain.map c { toFun := fun x => x ∈ notBelow y, monotone' := h }) ≤ z
rw [ωSup_le_iff]
no goals
case H
α : Type u_1
inst✝ : OmegaCompletePartialOrder α
y : Scott α
h : Monotone (notBelow y)
c : Chain α
z : Prop
⊢ ↑{ toFun := fun x => x ∈ notBelow y, monotone' := h } (ωSup c) ≤ z ↔
    ∀ (i : ℕ), ↑(Chain.map c { toFun := fun x => x ∈ notBelow y, monotone' := h }) i ≤ z
simp only [ωSup_le_iff, notBelow, mem_setOf_eq, le_Prop_eq, OrderHom.coe_fun_mk, Chain.map_coe,
  Function.comp_apply, exists_imp, not_forall]
α : Type u_1
inst✝ : OmegaCompletePartialOrder α
y x y' : Scott α
h : x ≤ y'
⊢ notBelow y x ≤ notBelow y y'
α : Type u_1
inst✝ : OmegaCompletePartialOrder α
y : Scott α
⊢ Monotone (notBelow y)
intro x y' h
α : Type u_1
inst✝ : OmegaCompletePartialOrder α
y x y' : Scott α
h : x ≤ y'
⊢ ¬x ≤ y → ¬y' ≤ y
α : Type u_1
inst✝ : OmegaCompletePartialOrder α
y x y' : Scott α
h : x ≤ y'
⊢ notBelow y x ≤ notBelow y y'
simp only [notBelow, setOf, le_Prop_eq]
α : Type u_1
inst✝ : OmegaCompletePartialOrder α
y x y' : Scott α
h : x ≤ y'
h₀ : ¬x ≤ y
h₁ : y' ≤ y
⊢ False
α : Type u_1
inst✝ : OmegaCompletePartialOrder α
y x y' : Scott α
h : x ≤ y'
⊢ ¬x ≤ y → ¬y' ≤ y
intro h₀ h₁
no goals
α : Type u_1
inst✝ : OmegaCompletePartialOrder α
y x y' : Scott α
h : x ≤ y'
h₀ : ¬x ≤ y
h₁ : y' ≤ y
⊢ False
apply h₀ (le_trans h h₁)