Principles of bar induction and continuity on Baire space

Kawai, 2019

The paper mentions the Uniform Continuity principle UC that each continuous function

f : (ℕ → Bool) → ℕ

is uniformly continuous. We prove this. We then prove also that such a function must be bounded.

theorem UC {f : (ℕ → Bool) → ℕ} (hf : Continuous f) : UniformContinuous f

theorem getbound {X : Type} [TopologicalSpace X] [CompactSpace X] [Nonempty X] {U : ℕ → Set X} (hU : ∀ (i : ℕ), IsOpen (U i)) (h : Set.univ ⊆ ⋃ (a : ℕ), U a) : ∃ (k : ℕ), Set.univ ⊆ ⋃ (a : Fin k), U ↑a

theorem bounded_of_continuous_compact {X : Type} [TopologicalSpace X] [CompactSpace X] [Nonempty X] (f : X → ℕ) (hf : Continuous f) : ∃ (a : ℕ), ∀ (A : X), f A ≤ a

theorem bounded_of_continuous (f : (ℕ → Bool) → ℕ) (hf : Continuous f) : ∃ (a : ℕ), ∀ (A : ℕ → Bool), f A ≤ a