Commit 2025-03-17 06:31 698f8d1c

View on Github →

chore: split long file Topology.ContinuousOn (#23001)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Topology/Algebra/Indicator.lean

Modified Mathlib/Topology/Clopen.lean

Modified Mathlib/Topology/ContinuousOn.lean

deleted theorem Continuous.if

deleted theorem Continuous.if_const

deleted theorem Continuous.piecewise

deleted theorem ContinuousOn.if'

deleted theorem ContinuousOn.if

deleted theorem ContinuousOn.piecewise'

deleted theorem ContinuousOn.piecewise

deleted theorem IsOpen.ite'

deleted theorem IsOpen.ite

deleted theorem continuousAt_update_same

deleted theorem continuousOn_piecewise_ite'

deleted theorem continuousOn_piecewise_ite

deleted theorem continuousWithinAt_update_same

deleted theorem continuous_if'

deleted theorem continuous_if

deleted theorem continuous_if_const

deleted theorem continuous_piecewise

deleted theorem ite_inter_closure_compl_eq_of_inter_frontier_eq

deleted theorem ite_inter_closure_eq_of_inter_frontier_eq

Modified Mathlib/Topology/Inseparable.lean

Modified Mathlib/Topology/Irreducible.lean

Modified Mathlib/Topology/LocallyFinite.lean

Created Mathlib/Topology/Piecewise.lean

added theorem Continuous.if

added theorem Continuous.if_const

added theorem Continuous.piecewise

added theorem ContinuousOn.if'

added theorem ContinuousOn.if

added theorem ContinuousOn.piecewise'

added theorem ContinuousOn.piecewise

added theorem IsOpen.ite'

added theorem IsOpen.ite

added theorem continuousAt_update_same

added theorem continuousOn_piecewise_ite'

added theorem continuousOn_piecewise_ite

added theorem continuousWithinAt_update_same

added theorem continuous_if'

added theorem continuous_if

added theorem continuous_if_const

added theorem continuous_piecewise

added theorem ite_inter_closure_compl_eq_of_inter_frontier_eq

added theorem ite_inter_closure_eq_of_inter_frontier_eq

Modified Mathlib/Topology/Semicontinuous.lean

Modified Mathlib/Topology/Separation/Basic.lean

Modified Mathlib/Topology/UniformSpace/Basic.lean