Theorem continuousWithinAt_toIocMod_Iic

Modification history

2026-01-13 18:40

Mathlib/Topology/Instances/AddCircle/Defs.lean

feat(AddCircle/Defs): prove continuity of `toIocDiv` etc (#33525)

Added continuousWithinAt_toIocMod_Iic View on Github →