α : Type u
β : Type v
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
s : Set (α →o β)
hs : ∀ (f : α →o β), f ∈ s → Continuous f
c : Chain α
⊢ ↑(sSup s) (ωSup c) = ωSup (Chain.map c (sSup s))
α : Type u
β : Type v
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
s : Set (α →o β)
hs : ∀ (f : α →o β), f ∈ s → Continuous f
⊢ Continuous (sSup s)
intro c
case H
α : Type u
β : Type v
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
s : Set (α →o β)
hs : ∀ (f : α →o β), f ∈ s → Continuous f
c : Chain α
⊢ ∀ (c_1 : β), ↑(sSup s) (ωSup c) ≤ c_1 ↔ ωSup (Chain.map c (sSup s)) ≤ c_1
α : Type u
β : Type v
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
s : Set (α →o β)
hs : ∀ (f : α →o β), f ∈ s → Continuous f
c : Chain α
⊢ ↑(sSup s) (ωSup c) = ωSup (Chain.map c (sSup s))
apply eq_of_forall_ge_iff
case H
α : Type u
β : Type v
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
s : Set (α →o β)
hs : ∀ (f : α →o β), f ∈ s → Continuous f
c : Chain α
z : β
⊢ ↑(sSup s) (ωSup c) ≤ z ↔ ωSup (Chain.map c (sSup s)) ≤ z
case H
α : Type u
β : Type v
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
s : Set (α →o β)
hs : ∀ (f : α →o β), f ∈ s → Continuous f
c : Chain α
⊢ ∀ (c_1 : β), ↑(sSup s) (ωSup c) ≤ c_1 ↔ ωSup (Chain.map c (sSup s)) ≤ c_1
intro z
case H
α : Type u
β : Type v
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
s : Set (α →o β)
hs : ∀ (f : α →o β), f ∈ s → Continuous f
c : Chain α
z : β
⊢ (∀ (f : α →o β), f ∈ s → ∀ (n : ℕ), ↑f (↑c n) ≤ z) ↔ ∀ (n : ℕ) (f : α →o β), f ∈ s → ↑f (↑c n) ≤ z
case H
α : Type u
β : Type v
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
s : Set (α →o β)
hs : ∀ (f : α →o β), f ∈ s → Continuous f
c : Chain α
z : β
⊢ ↑(sSup s) (ωSup c) ≤ z ↔ ωSup (Chain.map c (sSup s)) ≤ z
suffices (∀ f ∈ s, ∀ (n), (f : _) (c n) ≤ z) ↔ ∀ (n), ∀ f ∈ s, (f : _) (c n) ≤ z by
  simpa (config := { contextual := true }) [ωSup_le_iff, hs _ _ _] using this
no goals
case H
α : Type u
β : Type v
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
s : Set (α →o β)
hs : ∀ (f : α →o β), f ∈ s → Continuous f
c : Chain α
z : β
⊢ (∀ (f : α →o β), f ∈ s → ∀ (n : ℕ), ↑f (↑c n) ≤ z) ↔ ∀ (n : ℕ) (f : α →o β), f ∈ s → ↑f (↑c n) ≤ z
exact ⟨fun H n f hf => H f hf n, fun H f hf n => H n f hf⟩
no goals
α : Type u
β : Type v
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
s : Set (α →o β)
hs : ∀ (f : α →o β), f ∈ s → Continuous f
c : Chain α
z : β
this : (∀ (f : α →o β), f ∈ s → ∀ (n : ℕ), ↑f (↑c n) ≤ z) ↔ ∀ (n : ℕ) (f : α →o β), f ∈ s → ↑f (↑c n) ≤ z
⊢ ↑(sSup s) (ωSup c) ≤ z ↔ ωSup (Chain.map c (sSup s)) ≤ z
simpa (config := { contextual := true }) [ωSup_le_iff, hs _ _ _] using this