Commit 2026-01-13 18:40 bc95e587

View on Github →

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

Estimated changes

Modified Mathlib/Topology/Instances/AddCircle/Defs.lean

added theorem continuousAt_toIcoDiv

modified theorem continuousAt_toIcoMod

added theorem continuousAt_toIocDiv

modified theorem continuousAt_toIocMod

added theorem continuousOn_toIcoDiv

added theorem continuousOn_toIocDiv

added theorem continuousWithinAt_toIcoDiv_Ici

added theorem continuousWithinAt_toIcoMod_Ici

added theorem continuousWithinAt_toIocDiv_Iic

added theorem continuousWithinAt_toIocMod_Iic

deleted theorem continuous_left_toIocMod

deleted theorem continuous_right_toIcoMod

added theorem eventuallyEq_toIcoDiv_nhds

added theorem eventuallyEq_toIcoDiv_nhdsGE

added theorem eventuallyEq_toIcoDiv_nhdsLT

added theorem eventuallyEq_toIocDiv_nhds

added theorem eventuallyEq_toIocDiv_nhdsGT

added theorem eventuallyEq_toIocDiv_nhdsLE

modified theorem toIcoMod_eventuallyEq_toIocMod