Peano curve

This file proves the existsence of a Peano curve -- continuous sujrective map from the interval [0, 1] onto the square [0, 1] × [0, 1].

theorem exists_long_peano_curve : ∃ (f : C(ℝ, ↑unitInterval × ↑unitInterval)), Set.SurjOn (⇑f) cantorSet Set.univ

There is a continuous function on ℝ that maps the Cantor set to the square.

theorem exists_peano_curve : ∃ (f : C(↑unitInterval, ↑unitInterval × ↑unitInterval)), Function.Surjective ⇑f

There is a continuous surjection from the interval to the square.