Commit 2025-11-20 14:55 f579ecf2

View on Github →

feat(Counterexamples): Peano curve (#26185) Prove the existence of a continuous surjection from unitInterval onto unitInterval × unitInterval.

Estimated changes

Modified Counterexamples.lean

Created Counterexamples/PeanoCurve.lean

added theorem exists_long_peano_curve

added theorem exists_peano_curve

Modified Mathlib/Analysis/Complex/Tietze.lean

Modified Mathlib/Topology/ContinuousMap/Basic.lean

modified theorem ContinuousMap.coe_restrict

Modified Mathlib/Topology/UnitInterval.lean

added theorem unitInterval.eq_closedBall