α : Type u_3
β : α → Type u_2
γ : Type u_1
inst✝¹ : (x : α) → OmegaCompletePartialOrder (β x)
inst✝ : OmegaCompletePartialOrder γ
f : γ → (x : α) → β x
hf : ∀ (x : α), Continuous' fun g => f g x
c : Chain γ
⊢ ↑{ toFun := f, monotone' := (_ : ∀ (x y : γ), x ≤ y → ∀ (a : α), (fun g => f g a) x ≤ (fun g => f g a) y) } (ωSup c) =
    ωSup
      (map c { toFun := f, monotone' := (_ : ∀ (x y : γ), x ≤ y → ∀ (a : α), (fun g => f g a) x ≤ (fun g => f g a) y) })
α : Type u_3
β : α → Type u_2
γ : Type u_1
inst✝¹ : (x : α) → OmegaCompletePartialOrder (β x)
inst✝ : OmegaCompletePartialOrder γ
f : γ → (x : α) → β x
hf : ∀ (x : α), Continuous' fun g => f g x
⊢ Continuous { toFun := f, monotone' := (_ : ∀ (x y : γ), x ≤ y → ∀ (a : α), (fun g => f g a) x ≤ (fun g => f g a) y) }
intro c
case h
α : Type u_3
β : α → Type u_2
γ : Type u_1
inst✝¹ : (x : α) → OmegaCompletePartialOrder (β x)
inst✝ : OmegaCompletePartialOrder γ
f : γ → (x : α) → β x
hf : ∀ (x : α), Continuous' fun g => f g x
c : Chain γ
a : α
⊢ ↑{ toFun := f, monotone' := (_ : ∀ (x y : γ), x ≤ y → ∀ (a : α), (fun g => f g a) x ≤ (fun g => f g a) y) } (ωSup c)
      a =
    ωSup
      (map c { toFun := f, monotone' := (_ : ∀ (x y : γ), x ≤ y → ∀ (a : α), (fun g => f g a) x ≤ (fun g => f g a) y) })
      a
α : Type u_3
β : α → Type u_2
γ : Type u_1
inst✝¹ : (x : α) → OmegaCompletePartialOrder (β x)
inst✝ : OmegaCompletePartialOrder γ
f : γ → (x : α) → β x
hf : ∀ (x : α), Continuous' fun g => f g x
c : Chain γ
⊢ ↑{ toFun := f, monotone' := (_ : ∀ (x y : γ), x ≤ y → ∀ (a : α), (fun g => f g a) x ≤ (fun g => f g a) y) } (ωSup c) =
    ωSup
      (map c { toFun := f, monotone' := (_ : ∀ (x y : γ), x ≤ y → ∀ (a : α), (fun g => f g a) x ≤ (fun g => f g a) y) })
ext a
no goals
case h
α : Type u_3
β : α → Type u_2
γ : Type u_1
inst✝¹ : (x : α) → OmegaCompletePartialOrder (β x)
inst✝ : OmegaCompletePartialOrder γ
f : γ → (x : α) → β x
hf : ∀ (x : α), Continuous' fun g => f g x
c : Chain γ
a : α
⊢ ↑{ toFun := f, monotone' := (_ : ∀ (x y : γ), x ≤ y → ∀ (a : α), (fun g => f g a) x ≤ (fun g => f g a) y) } (ωSup c)
      a =
    ωSup
      (map c { toFun := f, monotone' := (_ : ∀ (x y : γ), x ≤ y → ∀ (a : α), (fun g => f g a) x ≤ (fun g => f g a) y) })
      a
apply (hf a).to_bundled _ c