Spreen spaces and the synthetic Kreisel-Lacombe-Shoenfield-Tseitin theorem

Andrej Bauer

Code by ChatGPT, mostly.

def rosolini_sigma : Set Bool

Equations

• rosolini_sigma = {p : Bool | ∃ (f : ℕ → Bool), p = true ↔ ∃ (n : ℕ), f n = true}

theorem rosolini_sigma_univ : rosolini_sigma = Set.univ