SequenceContinuity
Todd Waugh Ambridge, January 2024
# Uniform continuity of sequence functions
{-# OPTIONS --without-K --safe #-}
open import MLTT.Spartan
open import Notation.Order
open import Naturals.Order
open import UF.DiscreteAndSeparated
open import UF.FunExt
module TWA.Thesis.Chapter6.SequenceContinuity (fe : FunExt) where
open import TWA.Thesis.Chapter2.Sequences
open import TWA.Thesis.Chapter3.ClosenessSpaces fe
open import TWA.Thesis.Chapter3.ClosenessSpaces-Examples fe
open import MLTT.Two-Properties
seq-f-ucontinuous¹ : {X : 𝓤 ̇ } {Y : 𝓥 ̇ }
→ (f : (ℕ → X) → (ℕ → Y))
→ 𝓤 ⊔ 𝓥 ̇
seq-f-ucontinuous¹ {𝓤} {𝓥} {X} f
= (ϵ : ℕ) → Σ δ ꞉ ℕ , ((x₁ x₂ : (ℕ → X))
→ (x₁ ∼ⁿ x₂) δ → (f x₁ ∼ⁿ f x₂) ϵ)
seq-f-ucontinuous² : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } {Z : 𝓦 ̇ }
→ (f : (ℕ → X) → (ℕ → Y) → (ℕ → Z))
→ 𝓤 ⊔ 𝓥 ⊔ 𝓦 ̇
seq-f-ucontinuous² {𝓤} {𝓥} {𝓦} {X} {Y} f
= (ϵ : ℕ) → Σ (δˣ , δʸ) ꞉ ℕ × ℕ ,
((x₁ x₂ : (ℕ → X)) (y₁ y₂ : (ℕ → Y))
→ (x₁ ∼ⁿ x₂) δˣ → (y₁ ∼ⁿ y₂) δʸ → (f x₁ y₁ ∼ⁿ f x₂ y₂) ϵ)
map-ucontinuous' : {X : 𝓤 ̇ } {Y : 𝓥 ̇ }
→ (f : X → Y) → seq-f-ucontinuous¹ (map f)
map-ucontinuous' f ε = ε , λ α β α∼ⁿβ k k<ε → ap f (α∼ⁿβ k k<ε)
zipWith-ucontinuous' : {X : 𝓤 ̇ } {Y : 𝓥 ̇ }
→ (f : X → X → Y)
→ seq-f-ucontinuous² (zipWith f)
zipWith-ucontinuous' f ε
= (ε , ε)
, (λ α₁ α₂ β₁ β₂ α∼ β∼ k k<ϵ
→ ap (λ - → f - (β₁ k)) (α∼ k k<ϵ)
∙ ap (f (α₂ k)) (β∼ k k<ϵ))
seq-f-ucontinuous²-left : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } {Z : 𝓦 ̇ }
→ (f : (ℕ → X) → (ℕ → Y) → (ℕ → Z))
→ seq-f-ucontinuous² f
→ (β : ℕ → Y)
→ seq-f-ucontinuous¹ (λ α → f α β)
seq-f-ucontinuous²-left f ϕ β ε
= pr₁ (pr₁ (ϕ ε))
, λ α₁ α₂ α∼ → pr₂ (ϕ ε) α₁ α₂ β β α∼ (λ _ _ → refl)
seq-f-ucontinuous²-right : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } {Z : 𝓦 ̇ }
→ (f : (ℕ → X) → (ℕ → Y) → (ℕ → Z))
→ seq-f-ucontinuous² f
→ (α : ℕ → X)
→ seq-f-ucontinuous¹ (f α)
seq-f-ucontinuous²-right f ϕ α ε
= pr₂ (pr₁ (ϕ ε))
, λ β₁ β₂ → pr₂ (ϕ ε) α α β₁ β₂ (λ _ _ → refl)
seq-f-ucontinuous²-both : {X : 𝓤 ̇ } {Y : 𝓥 ̇ }
→ (f : (ℕ → X) → (ℕ → X) → (ℕ → Y))
→ seq-f-ucontinuous² f
→ seq-f-ucontinuous¹ (λ α → f α α)
seq-f-ucontinuous²-both f ϕ ε
= δ
, λ α β α∼ᵐβ → pr₂ (ϕ ε) α β α β
(λ i i<m → α∼ᵐβ i
(<-≤-trans i δ₁ δ i<m (max-≤-upper-bound δ₁ δ₂)))
(λ i i<m → α∼ᵐβ i
(<-≤-trans i δ₂ δ i<m (max-≤-upper-bound' δ₂ δ₁)))
where
δ₁ δ₂ δ : ℕ
δ₁ = pr₁ (pr₁ (ϕ ε))
δ₂ = pr₂ (pr₁ (ϕ ε))
δ = max δ₁ δ₂
seq-f-ucontinuous²-comp
: {X : 𝓤 ̇ } {Y : 𝓥 ̇ } {Z : 𝓦 ̇ } {W : 𝓣 ̇ } {T : 𝓤' ̇ }
→ (f : (ℕ → X) → (ℕ → W) → (ℕ → T))
→ (g : (ℕ → Y) → (ℕ → Z) → (ℕ → W))
→ seq-f-ucontinuous² f
→ seq-f-ucontinuous² g
→ (z : ℕ → Z) → seq-f-ucontinuous² λ x y → f x (g y z)
seq-f-ucontinuous²-comp
{_} {_} {_} {_} {_} {X} {Y} {Z} {W} {T} f g ϕᶠ ϕᵍ z ϵ = δ , γ
where
δ : ℕ × ℕ
δ = (pr₁ (pr₁ (ϕᶠ ϵ))) , pr₁ (pr₁ (ϕᵍ (pr₂ (pr₁ (ϕᶠ ϵ)))))
γ : (x₁ x₂ : ℕ → X) (y₁ y₂ : ℕ → Y)
→ (x₁ ∼ⁿ x₂) (pr₁ δ)
→ (y₁ ∼ⁿ y₂) (pr₂ δ)
→ (f x₁ (g y₁ z) ∼ⁿ f x₂ (g y₂ z)) ϵ
γ x₁ x₂ y₁ y₂ x₁∼x₂ y₁∼y₂
= pr₂ (ϕᶠ ϵ) x₁ x₂ (g y₁ z) (g y₂ z)
x₁∼x₂
(pr₂ (ϕᵍ (pr₂ (pr₁ (ϕᶠ ϵ)))) y₁ y₂ z z
y₁∼y₂
(λ _ _ → refl))
seq-f-ucontinuous¹²-comp
: {X : 𝓤 ̇ } {Y : 𝓥 ̇ } {Z : 𝓦 ̇ } {W : 𝓣 ̇ }
→ (f : (ℕ → Z) → (ℕ → W))
→ (g : (ℕ → X) → (ℕ → Y) → (ℕ → Z))
→ seq-f-ucontinuous¹ f
→ seq-f-ucontinuous² g
→ seq-f-ucontinuous² λ x y → f (g x y)
seq-f-ucontinuous¹²-comp {_} {_} {_} {_} {X} {Y} {Z} {W}
f g ϕᶠ ϕᵍ ϵ = δ , γ
where
δ : ℕ × ℕ
δ = pr₁ (ϕᵍ (pr₁ (ϕᶠ ϵ)))
γ : (x₁ x₂ : ℕ → X) (y₁ y₂ : ℕ → Y)
→ (x₁ ∼ⁿ x₂) (pr₁ δ) → (y₁ ∼ⁿ y₂) (pr₂ δ)
→ (f (g x₁ y₁) ∼ⁿ f (g x₂ y₂)) ϵ
γ x₁ x₂ y₁ y₂ x∼ y∼
= pr₂ (ϕᶠ ϵ) (g x₁ y₁) (g x₂ y₂)
(pr₂ (ϕᵍ (pr₁ (ϕᶠ ϵ))) x₁ x₂ y₁ y₂ x∼ y∼)
seq-f-ucontinuous²¹-comp-left
: {X : 𝓤 ̇ } {Y : 𝓥 ̇ } {Z : 𝓦 ̇ } {W : 𝓣 ̇ }
→ (f : (ℕ → W) → (ℕ → Y) → (ℕ → Z))
→ (g : (ℕ → X) → (ℕ → W))
→ seq-f-ucontinuous² f
→ seq-f-ucontinuous¹ g
→ seq-f-ucontinuous² (λ x y → f (g x) y)
seq-f-ucontinuous²¹-comp-left {_} {_} {_} {_} {X} {Y} {Z} {W}
f g ϕᶠ ϕᵍ ϵ = δ , γ
where
δ : ℕ × ℕ
δ = pr₁ (ϕᵍ (pr₁ (pr₁ (ϕᶠ ϵ)))) , (pr₂ (pr₁ (ϕᶠ ϵ)))
γ : (x₁ x₂ : ℕ → X) (y₁ y₂ : ℕ → Y)
→ (x₁ ∼ⁿ x₂) (pr₁ δ) → (y₁ ∼ⁿ y₂) (pr₂ δ)
→ (f (g x₁) y₁ ∼ⁿ f (g x₂) y₂) ϵ
γ x₁ x₂ y₁ y₂ x∼ y∼
= pr₂ (ϕᶠ ϵ) (g x₁) (g x₂) y₁ y₂
(pr₂ (ϕᵍ (pr₁ (pr₁ (ϕᶠ ϵ)))) x₁ x₂ x∼) y∼
seq-f-ucontinuousᴺ : {X : 𝓤 ̇ } {Y : 𝓥 ̇ }
→ (f : (ℕ → (ℕ → X)) → (ℕ → Y))
→ 𝓤 ⊔ 𝓥 ̇
seq-f-ucontinuousᴺ {𝓤} {𝓥} {X} f
= (ϵ : ℕ) → Σ (d , δ) ꞉ ℕ × ℕ , (d ≤ δ
× ((x₁ x₂ : (ℕ → (ℕ → X)))
→ ((n : ℕ) → n < d → (x₁ n ∼ⁿ x₂ n) δ) → (f x₁ ∼ⁿ f x₂) ϵ))
seq-f-ucontinuous¹-to-closeness
: {X : 𝓤 ̇ } {Y : 𝓥 ̇ }
→ (dˣ : is-discrete X) (dʸ : is-discrete Y)
→ (f : (ℕ → X) → (ℕ → Y))
→ seq-f-ucontinuous¹ f
→ f-ucontinuous (ℕ→D-ClosenessSpace dˣ) (ℕ→D-ClosenessSpace dʸ) f
seq-f-ucontinuous¹-to-closeness dˣ dʸ f ϕ ε
= pr₁ (ϕ ε)
, λ α β Cαβ → ∼ⁿ-to-C dʸ (f α) (f β) ε
(pr₂ (ϕ ε) α β (C-to-∼ⁿ dˣ α β (pr₁ (ϕ ε)) Cαβ))
closeness-to-seq-f-ucontinuous¹
: {X : 𝓤 ̇ } {Y : 𝓥 ̇ }
→ (dˣ : is-discrete X) (dʸ : is-discrete Y)
→ (f : (ℕ → X) → (ℕ → Y))
→ f-ucontinuous (ℕ→D-ClosenessSpace dˣ) (ℕ→D-ClosenessSpace dʸ) f
→ seq-f-ucontinuous¹ f
closeness-to-seq-f-ucontinuous¹ dˣ dʸ f ϕ ε
= pr₁ (ϕ ε)
, λ α β α∼β → C-to-∼ⁿ dʸ (f α) (f β) ε
(pr₂ (ϕ ε) α β (∼ⁿ-to-C dˣ α β (pr₁ (ϕ ε)) α∼β))
seq-f-ucontinuous¹-↔-closeness
: {X : 𝓤 ̇ } {Y : 𝓥 ̇ }
→ (dˣ : is-discrete X) (dʸ : is-discrete Y)
→ (f : (ℕ → X) → (ℕ → Y))
→ seq-f-ucontinuous¹ f
↔ f-ucontinuous (ℕ→D-ClosenessSpace dˣ) (ℕ→D-ClosenessSpace dʸ) f
seq-f-ucontinuous¹-↔-closeness dˣ dʸ f
= seq-f-ucontinuous¹-to-closeness dˣ dʸ f
, closeness-to-seq-f-ucontinuous¹ dˣ dʸ f
seq-f-ucontinuous²-to-closeness
: {X : 𝓤 ̇ } {Y : 𝓥 ̇ } {Z : 𝓦 ̇ }
→ (dˣ : is-discrete X) (dʸ : is-discrete Y) (dᶻ : is-discrete Z)
→ (f : (ℕ → X) → (ℕ → Y) → (ℕ → Z))
→ seq-f-ucontinuous² f
→ f-ucontinuous (×-ClosenessSpace (ℕ→D-ClosenessSpace dˣ)
(ℕ→D-ClosenessSpace dʸ))
(ℕ→D-ClosenessSpace dᶻ) (uncurry f)
seq-f-ucontinuous²-to-closeness dˣ dʸ dᶻ f ϕ ε
= δ
, λ (α₁ , α₂) (β₁ , β₂) Cαβ
→ ∼ⁿ-to-C dᶻ (f α₁ α₂) (f β₁ β₂) ε
(pr₂ (ϕ ε) α₁ β₁ α₂ β₂
(λ i i<δα → C-to-∼ⁿ dˣ α₁ β₁ δ
(×-C-left (ℕ→D-ClosenessSpace dˣ) (ℕ→D-ClosenessSpace dʸ)
α₁ β₁ α₂ β₂ δ Cαβ)
i (<-≤-trans i δα δ i<δα
(max-≤-upper-bound δα δβ)))
(λ i i<δβ → C-to-∼ⁿ dʸ α₂ β₂ δ
(×-C-right (ℕ→D-ClosenessSpace dˣ) (ℕ→D-ClosenessSpace dʸ)
α₁ β₁ α₂ β₂ δ Cαβ)
i (<-≤-trans i δβ δ i<δβ
(max-≤-upper-bound' δβ δα))))
where
δα δβ δ : ℕ
δα = pr₁ (pr₁ (ϕ ε))
δβ = pr₂ (pr₁ (ϕ ε))
δ = max δα δβ
closeness-to-seq-f-ucontinuous²
: {X : 𝓤 ̇ } {Y : 𝓥 ̇ } {Z : 𝓦 ̇ }
→ (dˣ : is-discrete X) (dʸ : is-discrete Y) (dᶻ : is-discrete Z)
→ (f : (ℕ → X) → (ℕ → Y) → (ℕ → Z))
→ f-ucontinuous (×-ClosenessSpace (ℕ→D-ClosenessSpace dˣ)
(ℕ→D-ClosenessSpace dʸ))
(ℕ→D-ClosenessSpace dᶻ) (uncurry f)
→ seq-f-ucontinuous² f
closeness-to-seq-f-ucontinuous² dˣ dʸ dᶻ f ϕ ε
= (δ , δ)
, λ x₁ x₂ y₁ y₂ x₁∼x₂ y₁∼y₂
→ C-to-∼ⁿ dᶻ (f x₁ y₁) (f x₂ y₂) ε
(pr₂ (ϕ ε) (x₁ , y₁) (x₂ , y₂)
(×-C-combine
(ℕ→D-ClosenessSpace dˣ) (ℕ→D-ClosenessSpace dʸ)
x₁ x₂ y₁ y₂ δ
(∼ⁿ-to-C dˣ x₁ x₂ δ x₁∼x₂) (∼ⁿ-to-C dʸ y₁ y₂ δ y₁∼y₂)))
where
δ : ℕ
δ = pr₁ (ϕ ε)
seq-f-ucontinuous²-↔-closeness
: {X : 𝓤 ̇ } {Y : 𝓥 ̇ } {Z : 𝓦 ̇ }
→ (dˣ : is-discrete X) (dʸ : is-discrete Y) (dᶻ : is-discrete Z)
→ (f : (ℕ → X) → (ℕ → Y) → (ℕ → Z))
→ seq-f-ucontinuous² f
↔ f-ucontinuous (×-ClosenessSpace (ℕ→D-ClosenessSpace dˣ)
(ℕ→D-ClosenessSpace dʸ))
(ℕ→D-ClosenessSpace dᶻ) (uncurry f)
seq-f-ucontinuous²-↔-closeness dˣ dʸ dᶻ f
= seq-f-ucontinuous²-to-closeness dˣ dʸ dᶻ f
, closeness-to-seq-f-ucontinuous² dˣ dʸ dᶻ f
pred : ℕ → ℕ
pred 0 = 0
pred (succ n) = n
double : ℕ → ℕ
double 0 = 0
double (succ n) = succ (succ (double n))
double-≤ : (n : ℕ) → n ≤ double n
double-≤ zero = ⋆
double-≤ (succ zero) = ⋆
double-≤ (succ (succ n))
= ≤-trans n (double n) (succ (succ (double n)))
(double-≤ n)
(≤-trans (double n) (succ (double n)) (succ (succ (double n)))
(≤-succ (double n)) (≤-succ (succ (double n))))
pred^i-0-is-0 : (i : ℕ) → (pred ^ i) 0 ＝ 0
pred^i-0-is-0 zero = refl
pred^i-0-is-0 (succ i) = ap pred (pred^i-0-is-0 i)
pred^si-sn-is-pred^i-n
: (i n : ℕ) → (pred ^ succ i) (succ n) ＝ (pred ^ i) n
pred^si-sn-is-pred^i-n zero n = refl
pred^si-sn-is-pred^i-n (succ i) n
= ap pred (pred^si-sn-is-pred^i-n i n)
pred^i≥n-is-0 : (i n : ℕ) → n ≤ i → (pred ^ i) n ＝ 0
pred^i≥n-is-0 i zero n≤i = pred^i-0-is-0 i
pred^i≥n-is-0 (succ i) (succ n) n≤i
= pred^si-sn-is-pred^i-n i n
∙ pred^i≥n-is-0 i n n≤i
pred^i-sn-is-s-pred^i-n
: (i n : ℕ) → i ≤ n → (pred ^ i) (succ n) ＝ succ ((pred ^ i) n)
pred^i-sn-is-s-pred^i-n zero n i<n = refl
pred^i-sn-is-s-pred^i-n (succ i) (succ n) i<n
= pred^si-sn-is-pred^i-n i (succ n)
∙ pred^i-sn-is-s-pred^i-n i n i<n
∙ ap succ (pred^si-sn-is-pred^i-n i n ⁻¹)
pred^n-double-n-is-n : (n : ℕ) → (pred ^ n) (double n) ＝ n
pred^n-double-n-is-n zero = refl
pred^n-double-n-is-n (succ n)
= pred^si-sn-is-pred^i-n n (succ (double n))
∙ pred^i-sn-is-s-pred^i-n n (double n) (double-≤ n)
∙ ap succ (pred^n-double-n-is-n n)
pred-≤ : (n : ℕ) → pred n ≤ n
pred-≤ zero = ⋆
pred-≤ (succ n) = ≤-succ n
predⁱ-≤ : (i n : ℕ) → (pred ^ i) n ≤ n
predⁱ-≤ zero n = ≤-refl n
predⁱ-≤ (succ i) n
= ≤-trans (pred ((pred ^ i) n)) ((pred ^ i) n) n
(pred-≤ ((pred ^ i) n)) (predⁱ-≤ i n)
pred-mono : (n m : ℕ) → n ≤ m → pred n ≤ pred m
pred-mono zero zero n≤m = ⋆
pred-mono zero (succ m) n≤m = ⋆
pred-mono (succ n) (succ m) n≤m = n≤m
nid : (n i d : ℕ) → n < i → (pred ^ i) d ≤ (pred ^ n) d
nid zero (succ i) d n<i = predⁱ-≤ (succ i) d
nid (succ n) (succ i) d n<i
= pred-mono ((pred ^ i) d) ((pred ^ n) d) (nid n i d n<i)
ΠC-to-∼ⁿ' : {X : ℕ → 𝓤 ̇ }
→ (d : (n : ℕ) → is-discrete (X n))
→ (α β : (ℕ → Π X)) (n : ℕ)
→ C (Π-ClosenessSpace (λ _ → ΠD-ClosenessSpace d)) n α β
→ (i : ℕ)
→ (α i ∼ⁿ β i) ((pred ^ i) n)
ΠC-to-∼ⁿ' d α β zero Cαβ i
= transport (α i ∼ⁿ β i) (pred^i-0-is-0 i ⁻¹) (λ _ ())
ΠC-to-∼ⁿ' d α β (succ n) Cαβ zero = C-to-∼ⁿ' d (α 0) (β 0) (succ n) γ
where
γ : C (ΠD-ClosenessSpace d) (succ n) (α 0) (β 0)
γ 0 j⊏sn = Cαβ 0 refl
γ (succ j) j⊏sn = Lemma[min𝟚ab＝₁→a＝₁] (Cαβ (succ j) j⊏sn)
ΠC-to-∼ⁿ' d α β (succ n) Cαβ (succ i)
= transport (α (succ i) ∼ⁿ β (succ i)) (pred^si-sn-is-pred^i-n i n ⁻¹) γ
where
γ : (α (succ i) ∼ⁿ β (succ i)) ((pred ^ i) n)
γ = ΠC-to-∼ⁿ' d (tail α) (tail β) n
(λ j j⊏n → Lemma[min𝟚ab＝₁→b＝₁] (Cαβ (succ j) j⊏n)) i
∼ⁿ-to-ΠC' : {X : ℕ → 𝓤 ̇ }
→ (d : (n : ℕ) → is-discrete (X n))
→ (α β : (ℕ → Π X)) (n : ℕ)
→ ((i : ℕ) → (α i ∼ⁿ β i) ((pred ^ i) n))
→ C (Π-ClosenessSpace (λ _ → ΠD-ClosenessSpace d)) n α β
∼ⁿ-to-ΠC' d α β n f 0 i⊏sn
= ∼ⁿ-to-C' d (α 0) (β 0) n (f 0) 0 i⊏sn
∼ⁿ-to-ΠC' d α β (succ n) f (succ i) i⊏sn
= Lemma[a＝₁→b＝₁→min𝟚ab＝₁]
(∼ⁿ-to-C' d (α 0) (β 0) (succ n) (f 0) (succ i) i⊏sn)
(∼ⁿ-to-ΠC' d (tail α) (tail β) n γ i i⊏sn)
where
γ : (j : ℕ) → (α (succ j) ∼ⁿ β (succ j)) ((pred ^ j) n)
γ j = transport (α (succ j) ∼ⁿ β (succ j))
(pred^si-sn-is-pred^i-n j n)
(f (succ j))
ΠC-to-∼ⁿ : {X : ℕ → 𝓤 ̇ }
→ (d : (n : ℕ) → is-discrete (X n))
→ (α β : (ℕ → Π X)) (n : ℕ)
→ C (Π-ClosenessSpace (λ _ → ΠD-ClosenessSpace d)) (double n) α β
→ (i : ℕ) → i < n → (α i ∼ⁿ β i) n
ΠC-to-∼ⁿ d α β n@(succ _) Cαβ i i<n j j<n
= ΠC-to-∼ⁿ' d α β (double n) Cαβ i j
(<-≤-trans j n ((pred ^ i) (double n)) j<n
(≤-trans n ((pred ^ n) (double n)) ((pred ^ i) (double n))
(transport (n ≤_) (pred^n-double-n-is-n n ⁻¹) (≤-refl n ))
(nid i n (double n) i<n)))
∼ⁿ-to-ΠC : {X : ℕ → 𝓤 ̇ }
→ (d : (n : ℕ) → is-discrete (X n))
→ (α β : (ℕ → Π X)) (n : ℕ)
→ ((i : ℕ) → i < n → (α i ∼ⁿ β i) n)
→ C (Π-ClosenessSpace (λ _ → ΠD-ClosenessSpace d)) n α β
∼ⁿ-to-ΠC d α β n@(succ _) α∼β
= ∼ⁿ-to-ΠC' d α β n (λ i → Cases (order-split i n) (γ< i) (γ≥ i))
where
γ< : (i : ℕ) → i < n → (α i ∼ⁿ β i) ((pred ^ i) n)
γ< i i<n j j<2n-i
= α∼β i i<n j (<-≤-trans j ((pred ^ i) n) n j<2n-i (predⁱ-≤ i n))
γ≥ : (i : ℕ) → n ≤ i → (α i ∼ⁿ β i) ((pred ^ i) n)
γ≥ i n≤i = transport (α i ∼ⁿ β i) (pred^i≥n-is-0 i n n≤i ⁻¹) (λ _ ())
seq-f-ucontinuousᴺ-to-closeness
: {X : 𝓤 ̇ } {Y : 𝓥 ̇ }
→ (dˣ : is-discrete X) (dʸ : is-discrete Y)
→ (f : (ℕ → (ℕ → X)) → (ℕ → Y))
→ seq-f-ucontinuousᴺ f
→ f-ucontinuous (Π-ClosenessSpace (λ _ → ℕ→D-ClosenessSpace dˣ))
(ℕ→D-ClosenessSpace dʸ) f
seq-f-ucontinuousᴺ-to-closeness {𝓤} {𝓥} {X} {Y} dˣ dʸ f ϕ ε
= double δ
, λ x₁ x₂ C2δx₁x₂ → ∼ⁿ-to-C' (λ _ → dʸ) (f x₁) (f x₂) ε
(ϕ' x₁ x₂ (λ n n<d
→ ΠC-to-∼ⁿ (λ _ → dˣ) x₁ x₂ δ C2δx₁x₂ n
(<-≤-trans n d δ n<d d≤δ)))
where
d δ : ℕ
d = pr₁ (pr₁ (ϕ ε))
δ = pr₂ (pr₁ (ϕ ε))
d≤δ : d ≤ δ
d≤δ = pr₁ (pr₂ (ϕ ε))
ϕ' : (x₁ x₂ : (ℕ → (ℕ → X)))
→ ((n : ℕ) → n < d → (x₁ n ∼ⁿ x₂ n) δ)
→ (f x₁ ∼ⁿ f x₂) ε
ϕ' = pr₂ (pr₂ (ϕ ε))
closeness-to-seq-f-ucontinuousᴺ
: {X : 𝓤 ̇ } {Y : 𝓥 ̇ }
→ (dˣ : is-discrete X) (dʸ : is-discrete Y)
→ (f : (ℕ → (ℕ → X)) → (ℕ → Y))
→ f-ucontinuous (Π-ClosenessSpace (λ _ → ℕ→D-ClosenessSpace dˣ))
(ℕ→D-ClosenessSpace dʸ) f
→ seq-f-ucontinuousᴺ f
closeness-to-seq-f-ucontinuousᴺ {𝓤} {𝓥} {X} {Y} dˣ dʸ f ϕ ε
= (δ , δ) , ≤-refl δ
, λ x₁ x₂ x₁∼x₂ → C-to-∼ⁿ' (λ _ → dʸ) (f x₁) (f x₂) ε
(pr₂ (ϕ ε) x₁ x₂ (∼ⁿ-to-ΠC (λ _ → dˣ) x₁ x₂ δ x₁∼x₂))
where
δ : ℕ
δ = pr₁ (ϕ ε)
seq-f-ucontinuousᴺ-↔-closeness
: {X : 𝓤 ̇ } {Y : 𝓥 ̇ }
→ (dˣ : is-discrete X) (dʸ : is-discrete Y)
→ (f : (ℕ → (ℕ → X)) → (ℕ → Y))
→ seq-f-ucontinuousᴺ f
↔ f-ucontinuous (Π-ClosenessSpace (λ _ → ℕ→D-ClosenessSpace dˣ))
(ℕ→D-ClosenessSpace dʸ) f
seq-f-ucontinuousᴺ-↔-closeness {𝓤} {𝓥} {X} {Y} dˣ dʸ f
= seq-f-ucontinuousᴺ-to-closeness dˣ dʸ f
, closeness-to-seq-f-ucontinuousᴺ dˣ dʸ f