α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
hf : ∀ (s : Set (Scott β)), IsOpen s → IsOpen {x | f x ∈ s}
h : Monotone f
⊢ Continuous' f
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
hf : ∀ (s : Set (Scott β)), IsOpen s → IsOpen {x | f x ∈ s}
⊢ Continuous' f
have h : Monotone f := by
  intro x y h
  cases' hf { x | ¬x ≤ f y } (notBelow_isOpen _) with hf hf'
  clear hf'
  specialize hf h
  simp only [preimage, mem_setOf_eq, le_Prop_eq] at hf
  by_contra H
  apply hf H le_rfl
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
hf : ∀ (s : Set (Scott β)), IsOpen s → IsOpen {x | f x ∈ s}
h : Monotone f
⊢ OmegaCompletePartialOrder.Continuous { toFun := f, monotone' := h }
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
hf : ∀ (s : Set (Scott β)), IsOpen s → IsOpen {x | f x ∈ s}
h : Monotone f
⊢ Continuous' f
exists h
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
hf : ∀ (s : Set (Scott β)), IsOpen s → IsOpen {x | f x ∈ s}
h : Monotone f
c : Chain (Scott α)
⊢ ↑{ toFun := f, monotone' := h } (ωSup c) = ωSup (Chain.map c { toFun := f, monotone' := h })
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
hf : ∀ (s : Set (Scott β)), IsOpen s → IsOpen {x | f x ∈ s}
h : Monotone f
⊢ OmegaCompletePartialOrder.Continuous { toFun := f, monotone' := h }
intro c
case H
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
hf : ∀ (s : Set (Scott β)), IsOpen s → IsOpen {x | f x ∈ s}
h : Monotone f
c : Chain (Scott α)
⊢ ∀ (c_1 : Scott β),
    ↑{ toFun := f, monotone' := h } (ωSup c) ≤ c_1 ↔ ωSup (Chain.map c { toFun := f, monotone' := h }) ≤ c_1
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
hf : ∀ (s : Set (Scott β)), IsOpen s → IsOpen {x | f x ∈ s}
h : Monotone f
c : Chain (Scott α)
⊢ ↑{ toFun := f, monotone' := h } (ωSup c) = ωSup (Chain.map c { toFun := f, monotone' := h })
apply eq_of_forall_ge_iff
case H
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
hf : ∀ (s : Set (Scott β)), IsOpen s → IsOpen {x | f x ∈ s}
h : Monotone f
c : Chain (Scott α)
z : Scott β
⊢ ↑{ toFun := f, monotone' := h } (ωSup c) ≤ z ↔ ωSup (Chain.map c { toFun := f, monotone' := h }) ≤ z
case H
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
hf : ∀ (s : Set (Scott β)), IsOpen s → IsOpen {x | f x ∈ s}
h : Monotone f
c : Chain (Scott α)
⊢ ∀ (c_1 : Scott β),
    ↑{ toFun := f, monotone' := h } (ωSup c) ≤ c_1 ↔ ωSup (Chain.map c { toFun := f, monotone' := h }) ≤ c_1
intro z
case H
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
h : Monotone f
c : Chain (Scott α)
z : Scott β
hf : IsOpen {x | f x ∈ notBelow z}
⊢ ↑{ toFun := f, monotone' := h } (ωSup c) ≤ z ↔ ωSup (Chain.map c { toFun := f, monotone' := h }) ≤ z
case H
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
hf : ∀ (s : Set (Scott β)), IsOpen s → IsOpen {x | f x ∈ s}
h : Monotone f
c : Chain (Scott α)
z : Scott β
⊢ ↑{ toFun := f, monotone' := h } (ωSup c) ≤ z ↔ ωSup (Chain.map c { toFun := f, monotone' := h }) ≤ z
specialize hf _ (notBelow_isOpen z)
case H.intro
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
h : Monotone f
c : Chain (Scott α)
z : Scott β
w✝ : Monotone fun x => x ∈ {x | f x ∈ notBelow z}
hf_h : OmegaCompletePartialOrder.Continuous { toFun := fun x => x ∈ {x | f x ∈ notBelow z}, monotone' := w✝ }
⊢ ↑{ toFun := f, monotone' := h } (ωSup c) ≤ z ↔ ωSup (Chain.map c { toFun := f, monotone' := h }) ≤ z
case H
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
h : Monotone f
c : Chain (Scott α)
z : Scott β
hf : IsOpen {x | f x ∈ notBelow z}
⊢ ↑{ toFun := f, monotone' := h } (ωSup c) ≤ z ↔ ωSup (Chain.map c { toFun := f, monotone' := h }) ≤ z
cases' hf with _ hf_h
case H.intro
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
h : Monotone f
c : Chain (Scott α)
z : Scott β
w✝ : Monotone fun x => x ∈ {x | f x ∈ notBelow z}
hf_h :
  ↑{ toFun := fun x => x ∈ {x | f x ∈ notBelow z}, monotone' := w✝ } (ωSup c) =
    ωSup (Chain.map c { toFun := fun x => x ∈ {x | f x ∈ notBelow z}, monotone' := w✝ })
⊢ ↑{ toFun := f, monotone' := h } (ωSup c) ≤ z ↔ ωSup (Chain.map c { toFun := f, monotone' := h }) ≤ z
case H.intro
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
h : Monotone f
c : Chain (Scott α)
z : Scott β
w✝ : Monotone fun x => x ∈ {x | f x ∈ notBelow z}
hf_h : OmegaCompletePartialOrder.Continuous { toFun := fun x => x ∈ {x | f x ∈ notBelow z}, monotone' := w✝ }
⊢ ↑{ toFun := f, monotone' := h } (ωSup c) ≤ z ↔ ωSup (Chain.map c { toFun := f, monotone' := h }) ≤ z
specialize hf_h c
case H.intro
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
h : Monotone f
c : Chain (Scott α)
z : Scott β
w✝ : Monotone fun x => x ∈ {x | f x ∈ notBelow z}
hf_h :
  ¬f (ωSup c) ≤ z ↔ ωSup (Chain.map c { toFun := fun x => ¬f x ≤ z, monotone' := (_ : Monotone fun x => ¬f x ≤ z) })
⊢ ↑{ toFun := f, monotone' := h } (ωSup c) ≤ z ↔ ωSup (Chain.map c { toFun := f, monotone' := h }) ≤ z
case H.intro
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
h : Monotone f
c : Chain (Scott α)
z : Scott β
w✝ : Monotone fun x => x ∈ {x | f x ∈ notBelow z}
hf_h :
  ↑{ toFun := fun x => x ∈ {x | f x ∈ notBelow z}, monotone' := w✝ } (ωSup c) =
    ωSup (Chain.map c { toFun := fun x => x ∈ {x | f x ∈ notBelow z}, monotone' := w✝ })
⊢ ↑{ toFun := f, monotone' := h } (ωSup c) ≤ z ↔ ωSup (Chain.map c { toFun := f, monotone' := h }) ≤ z
simp only [notBelow, eq_iff_iff, mem_setOf_eq] at hf_h
case H.intro
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
h : Monotone f
c : Chain (Scott α)
z : Scott β
w✝ : Monotone fun x => x ∈ {x | f x ∈ notBelow z}
hf_h :
  ¬f (ωSup c) ≤ z ↔ ωSup (Chain.map c { toFun := fun x => ¬f x ≤ z, monotone' := (_ : Monotone fun x => ¬f x ≤ z) })
⊢ ¬↑{ toFun := f, monotone' := h } (ωSup c) ≤ z ↔ ¬ωSup (Chain.map c { toFun := f, monotone' := h }) ≤ z
case H.intro
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
h : Monotone f
c : Chain (Scott α)
z : Scott β
w✝ : Monotone fun x => x ∈ {x | f x ∈ notBelow z}
hf_h :
  ¬f (ωSup c) ≤ z ↔ ωSup (Chain.map c { toFun := fun x => ¬f x ≤ z, monotone' := (_ : Monotone fun x => ¬f x ≤ z) })
⊢ ↑{ toFun := f, monotone' := h } (ωSup c) ≤ z ↔ ωSup (Chain.map c { toFun := f, monotone' := h }) ≤ z
rw [← not_iff_not]
case H.intro
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
h : Monotone f
c : Chain (Scott α)
z : Scott β
w✝ : Monotone fun x => x ∈ {x | f x ∈ notBelow z}
hf_h :
  ¬f (ωSup c) ≤ z ↔ ωSup (Chain.map c { toFun := fun x => ¬f x ≤ z, monotone' := (_ : Monotone fun x => ¬f x ≤ z) })
⊢ (∃ a, (∃ y, ¬f (↑c y) ≤ z ↔ a) ∧ a) ↔ ∃ x, ¬f (↑c x) ≤ z
case H.intro
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
h : Monotone f
c : Chain (Scott α)
z : Scott β
w✝ : Monotone fun x => x ∈ {x | f x ∈ notBelow z}
hf_h :
  ¬f (ωSup c) ≤ z ↔ ωSup (Chain.map c { toFun := fun x => ¬f x ≤ z, monotone' := (_ : Monotone fun x => ¬f x ≤ z) })
⊢ ¬↑{ toFun := f, monotone' := h } (ωSup c) ≤ z ↔ ¬ωSup (Chain.map c { toFun := f, monotone' := h }) ≤ z
simp only [ωSup_le_iff, hf_h, ωSup, iSup, sSup, mem_range, Chain.map_coe, Function.comp_apply,
  eq_iff_iff, not_forall]
no goals
case H.intro
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
h : Monotone f
c : Chain (Scott α)
z : Scott β
w✝ : Monotone fun x => x ∈ {x | f x ∈ notBelow z}
hf_h :
  ¬f (ωSup c) ≤ z ↔ ωSup (Chain.map c { toFun := fun x => ¬f x ≤ z, monotone' := (_ : Monotone fun x => ¬f x ≤ z) })
⊢ (∃ a, (∃ y, ¬f (↑c y) ≤ z ↔ a) ∧ a) ↔ ∃ x, ¬f (↑c x) ≤ z
tauto
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
hf : ∀ (s : Set (Scott β)), IsOpen s → IsOpen {x | f x ∈ s}
x y : Scott α
h : x ≤ y
⊢ f x ≤ f y
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
hf : ∀ (s : Set (Scott β)), IsOpen s → IsOpen {x | f x ∈ s}
⊢ Monotone f
intro x y h
case intro
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
hf✝ : ∀ (s : Set (Scott β)), IsOpen s → IsOpen {x | f x ∈ s}
x y : Scott α
h : x ≤ y
hf : Monotone fun x => x ∈ {x | f x ∈ {x | ¬x ≤ f y}}
hf' : OmegaCompletePartialOrder.Continuous { toFun := fun x => x ∈ {x | f x ∈ {x | ¬x ≤ f y}}, monotone' := hf }
⊢ f x ≤ f y
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
hf : ∀ (s : Set (Scott β)), IsOpen s → IsOpen {x | f x ∈ s}
x y : Scott α
h : x ≤ y
⊢ f x ≤ f y
cases' hf { x | ¬x ≤ f y } (notBelow_isOpen _) with hf hf'
case intro
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
hf✝ : ∀ (s : Set (Scott β)), IsOpen s → IsOpen {x | f x ∈ s}
x y : Scott α
h : x ≤ y
hf : Monotone fun x => x ∈ {x | f x ∈ {x | ¬x ≤ f y}}
⊢ f x ≤ f y
case intro
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
hf✝ : ∀ (s : Set (Scott β)), IsOpen s → IsOpen {x | f x ∈ s}
x y : Scott α
h : x ≤ y
hf : Monotone fun x => x ∈ {x | f x ∈ {x | ¬x ≤ f y}}
hf' : OmegaCompletePartialOrder.Continuous { toFun := fun x => x ∈ {x | f x ∈ {x | ¬x ≤ f y}}, monotone' := hf }
⊢ f x ≤ f y
clear hf'
case intro
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
hf✝ : ∀ (s : Set (Scott β)), IsOpen s → IsOpen {x | f x ∈ s}
x y : Scott α
h : x ≤ y
hf : (fun x => x ∈ {x | f x ∈ {x | ¬x ≤ f y}}) x ≤ (fun x => x ∈ {x | f x ∈ {x | ¬x ≤ f y}}) y
⊢ f x ≤ f y
case intro
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
hf✝ : ∀ (s : Set (Scott β)), IsOpen s → IsOpen {x | f x ∈ s}
x y : Scott α
h : x ≤ y
hf : Monotone fun x => x ∈ {x | f x ∈ {x | ¬x ≤ f y}}
⊢ f x ≤ f y
specialize hf h
case intro
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
hf✝ : ∀ (s : Set (Scott β)), IsOpen s → IsOpen {x | f x ∈ s}
x y : Scott α
h : x ≤ y
hf : ¬f x ≤ f y → ¬f y ≤ f y
⊢ f x ≤ f y
case intro
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
hf✝ : ∀ (s : Set (Scott β)), IsOpen s → IsOpen {x | f x ∈ s}
x y : Scott α
h : x ≤ y
hf : (fun x => x ∈ {x | f x ∈ {x | ¬x ≤ f y}}) x ≤ (fun x => x ∈ {x | f x ∈ {x | ¬x ≤ f y}}) y
⊢ f x ≤ f y
simp only [preimage, mem_setOf_eq, le_Prop_eq] at hf
case intro
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
hf✝ : ∀ (s : Set (Scott β)), IsOpen s → IsOpen {x | f x ∈ s}
x y : Scott α
h : x ≤ y
hf : ¬f x ≤ f y → ¬f y ≤ f y
H : ¬f x ≤ f y
⊢ False
case intro
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
hf✝ : ∀ (s : Set (Scott β)), IsOpen s → IsOpen {x | f x ∈ s}
x y : Scott α
h : x ≤ y
hf : ¬f x ≤ f y → ¬f y ≤ f y
⊢ f x ≤ f y
by_contra H
no goals
case intro
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
hf✝ : ∀ (s : Set (Scott β)), IsOpen s → IsOpen {x | f x ∈ s}
x y : Scott α
h : x ≤ y
hf : ¬f x ≤ f y → ¬f y ≤ f y
H : ¬f x ≤ f y
⊢ False
apply hf H le_rfl