[GOAL]
α : Type u
inst✝ : Preorder α
c : Chain α
x : α
⊢ IsωSup c x ↔ IsLUB (range ↑c) x
[PROOFSTEP]
simp [IsωSup, IsLUB, IsLeast, upperBounds, lowerBounds]
[GOAL]
α : Type u
inst✝ : OmegaCompletePartialOrder α
s : Set (Set α)
hs : ∀ (t : Set α), t ∈ s → IsOpen α t
⊢ IsOpen α (⋃₀ s)
[PROOFSTEP]
simp only [IsOpen] at hs ⊢
[GOAL]
α : Type u
inst✝ : OmegaCompletePartialOrder α
s : Set (Set α)
hs : ∀ (t : Set α), t ∈ s → Continuous' fun x => x ∈ t
⊢ Continuous' fun x => x ∈ ⋃₀ s
[PROOFSTEP]
convert CompleteLattice.sSup_continuous' (setOf ⁻¹' s) hs
[GOAL]
case h.e'_5.h.a
α : Type u
inst✝ : OmegaCompletePartialOrder α
s : Set (Set α)
hs : ∀ (t : Set α), t ∈ s → Continuous' fun x => x ∈ t
x✝ : α
⊢ x✝ ∈ ⋃₀ s ↔ sSup (setOf ⁻¹' s) x✝
[PROOFSTEP]
simp only [sSup_apply, setOf_bijective.surjective.exists, exists_prop, mem_preimage, SetCoe.exists, iSup_Prop_eq,
  mem_setOf_eq, mem_sUnion]
[GOAL]
α : Type u_1
inst✝ : OmegaCompletePartialOrder α
y : Scott α
⊢ IsOpen (notBelow y)
[PROOFSTEP]
have h : Monotone (notBelow y) := fun x z hle ↦ mt hle.trans
[GOAL]
α : Type u_1
inst✝ : OmegaCompletePartialOrder α
y : Scott α
h : Monotone (notBelow y)
⊢ IsOpen (notBelow y)
[PROOFSTEP]
refine ⟨h, fun c ↦ eq_of_forall_ge_iff fun z ↦ ?_⟩
[GOAL]
α : 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
[PROOFSTEP]
simp only [ωSup_le_iff, notBelow, mem_setOf_eq, le_Prop_eq, OrderHom.coe_mk, Chain.map_coe, Function.comp_apply,
  exists_imp, not_forall]
[GOAL]
α : Type u_1
inst✝ : OmegaCompletePartialOrder α
c : Chain α
⊢ IsωSup c (ωSup c)
[PROOFSTEP]
constructor
[GOAL]
case left
α : Type u_1
inst✝ : OmegaCompletePartialOrder α
c : Chain α
⊢ ∀ (i : ℕ), ↑c i ≤ ωSup c
[PROOFSTEP]
apply le_ωSup
[GOAL]
case right
α : Type u_1
inst✝ : OmegaCompletePartialOrder α
c : Chain α
⊢ ∀ (y : α), (∀ (i : ℕ), ↑c i ≤ y) → ωSup c ≤ y
[PROOFSTEP]
apply ωSup_le
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
hf : _root_.Continuous f
⊢ Continuous' f
[PROOFSTEP]
have h : Monotone f := fun x y h ↦
  by
  have hf : IsUpperSet {x | ¬f x ≤ f y} := ((notBelow_isOpen (f y)).preimage hf).isUpperSet
  simpa only [mem_setOf_eq, le_refl, not_true, imp_false, not_not] using hf h
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
hf : _root_.Continuous f
x y : Scott α
h : x ≤ y
⊢ f x ≤ f y
[PROOFSTEP]
have hf : IsUpperSet {x | ¬f x ≤ f y} := ((notBelow_isOpen (f y)).preimage hf).isUpperSet
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
hf✝ : _root_.Continuous f
x y : Scott α
h : x ≤ y
hf : IsUpperSet {x | ¬f x ≤ f y}
⊢ f x ≤ f y
[PROOFSTEP]
simpa only [mem_setOf_eq, le_refl, not_true, imp_false, not_not] using hf h
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
hf : _root_.Continuous f
h : Monotone f
⊢ Continuous' f
[PROOFSTEP]
refine ⟨h, fun c ↦ eq_of_forall_ge_iff fun z ↦ ?_⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
hf : _root_.Continuous f
h : Monotone f
c : Chain (Scott α)
z : Scott β
⊢ ↑{ toFun := f, monotone' := h } (ωSup c) ≤ z ↔ ωSup (Chain.map c { toFun := f, monotone' := h }) ≤ z
[PROOFSTEP]
rcases(notBelow_isOpen z).preimage hf with ⟨hf, hf'⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
hf✝ : _root_.Continuous f
h : Monotone f
c : Chain (Scott α)
z : Scott β
hf : Monotone fun x => x ∈ f ⁻¹' notBelow z
hf' : OmegaCompletePartialOrder.Continuous { toFun := fun x => x ∈ f ⁻¹' notBelow z, monotone' := hf }
⊢ ↑{ toFun := f, monotone' := h } (ωSup c) ≤ z ↔ ωSup (Chain.map c { toFun := f, monotone' := h }) ≤ z
[PROOFSTEP]
specialize hf' c
[GOAL]
case intro
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
hf✝ : _root_.Continuous f
h : Monotone f
c : Chain (Scott α)
z : Scott β
hf : Monotone fun x => x ∈ f ⁻¹' notBelow z
hf' :
  ↑{ toFun := fun x => x ∈ f ⁻¹' notBelow z, monotone' := hf } (ωSup c) =
    ωSup (Chain.map c { toFun := fun x => x ∈ f ⁻¹' notBelow z, monotone' := hf })
⊢ ↑{ toFun := f, monotone' := h } (ωSup c) ≤ z ↔ ωSup (Chain.map c { toFun := f, monotone' := h }) ≤ z
[PROOFSTEP]
simp only [OrderHom.coe_mk, mem_preimage, notBelow, mem_setOf_eq] at hf' 
[GOAL]
case intro
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
hf✝ : _root_.Continuous f
h : Monotone f
c : Chain (Scott α)
z : Scott β
hf : Monotone fun x => x ∈ f ⁻¹' notBelow z
hf' :
  (¬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
[PROOFSTEP]
rw [← not_iff_not]
[GOAL]
case intro
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
hf✝ : _root_.Continuous f
h : Monotone f
c : Chain (Scott α)
z : Scott β
hf : Monotone fun x => x ∈ f ⁻¹' notBelow z
hf' :
  (¬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
[PROOFSTEP]
simp only [ωSup_le_iff, hf', ωSup, iSup, sSup, mem_range, Chain.map_coe, Function.comp_apply, eq_iff_iff, not_forall,
  OrderHom.coe_mk]
[GOAL]
case intro
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
hf✝ : _root_.Continuous f
h : Monotone f
c : Chain (Scott α)
z : Scott β
hf : Monotone fun x => x ∈ f ⁻¹' notBelow z
hf' :
  (¬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
[PROOFSTEP]
tauto
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
hf : Continuous' f
⊢ _root_.Continuous f
[PROOFSTEP]
rw [continuous_def]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
hf : Continuous' f
⊢ ∀ (s : Set (Scott β)), IsOpen s → IsOpen (f ⁻¹' s)
[PROOFSTEP]
intro s hs
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
hf : Continuous' f
s : Set (Scott β)
hs : IsOpen s
⊢ IsOpen (f ⁻¹' s)
[PROOFSTEP]
change Continuous' (s ∘ f)
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
hf : Continuous' f
s : Set (Scott β)
hs : IsOpen s
⊢ Continuous' (s ∘ f)
[PROOFSTEP]
cases' hs with hs hs'
[GOAL]
case intro
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
hf : Continuous' f
s : Set (Scott β)
hs : Monotone fun x => x ∈ s
hs' : OmegaCompletePartialOrder.Continuous { toFun := fun x => x ∈ s, monotone' := hs }
⊢ Continuous' (s ∘ f)
[PROOFSTEP]
cases' hf with hf hf'
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
s : Set (Scott β)
hs : Monotone fun x => x ∈ s
hs' : OmegaCompletePartialOrder.Continuous { toFun := fun x => x ∈ s, monotone' := hs }
hf : Monotone f
hf' : OmegaCompletePartialOrder.Continuous { toFun := f, monotone' := hf }
⊢ Continuous' (s ∘ f)
[PROOFSTEP]
apply Continuous.of_bundled
[GOAL]
case intro.intro.hf'
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
s : Set (Scott β)
hs : Monotone fun x => x ∈ s
hs' : OmegaCompletePartialOrder.Continuous { toFun := fun x => x ∈ s, monotone' := hs }
hf : Monotone f
hf' : OmegaCompletePartialOrder.Continuous { toFun := f, monotone' := hf }
⊢ OmegaCompletePartialOrder.Continuous { toFun := s ∘ f, monotone' := ?intro.intro.hf }
case intro.intro.hf
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
s : Set (Scott β)
hs : Monotone fun x => x ∈ s
hs' : OmegaCompletePartialOrder.Continuous { toFun := fun x => x ∈ s, monotone' := hs }
hf : Monotone f
hf' : OmegaCompletePartialOrder.Continuous { toFun := f, monotone' := hf }
⊢ Monotone (s ∘ f)
[PROOFSTEP]
apply continuous_comp _ _ hf' hs'
