chore: rename `continuous{,On,At,Within}_const` to `ContinuousFoo.const` by grunweg · Pull Request #31607 · leanprover-community/mathlib4

grunweg · 2025-11-13T22:36:35Z

Zulip discussion: #mathlib4 > Naming convention @ 💬

depends on: [Merged by Bors] - chore: golf using fun_prop #34441
depends on: [Merged by Bors] - chore(Archive): small golfs #34688

github-actions · 2025-11-13T22:37:45Z

PR summary 56e100aabd

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ Continuous.const
+ ContinuousAt.const
+ ContinuousOn.const
+ ContinuousWithinAt.const

You can run this locally as follows

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

j-loreaux

I don't think any of these are required to be protected, because we don't have const in the root namespace. If you think it's better to do so, that's fine.

bors d+

j-loreaux · 2025-11-13T22:39:52Z

Mathlib/Analysis/Calculus/Deriv/MeanValue.lean

    ((hff' x hx).const_mul (g b - g a)).sub ((hgg' x hx).const_mul (f b - f a))
  have hhc : ContinuousOn h (Icc a b) :=
-    (continuousOn_const.mul hfc).sub (continuousOn_const.mul hgc)
+    (ContinuousOn.const.mul hfc).sub (ContinuousOn.const.mul hgc)


I'm not necessarily saying you should do this, but I expect this would work:

Suggested change

(ContinuousOn.const.mul hfc).sub (ContinuousOn.const.mul hgc)

.sub (.mul .const hfc) (.mul .const hgc)

mathlib-bors · 2025-11-15T04:40:17Z

✌️ grunweg can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

mathlib4-merge-conflict-bot · 2026-01-07T16:53:12Z

This pull request has conflicts, please merge master and resolve them.

The goal of this PR is to remove many explicit references to continuous(On)_const; to reduce the diff in leanprover-community#31607

The goal of this PR is to remove many explicit references to continuous(On)_const; to reduce the diff in #31607.

mathlib4-merge-conflict-bot · 2026-02-01T03:51:15Z

This pull request has conflicts, please merge master and resolve them.

Use fun_prop more, and make indentation match mathlib style better. Extracted from leanprover-community#31607.

Use fun_prop more, and make indentation match mathlib style better. Extracted from #31607.

mathlib4-dependent-issues-bot · 2026-02-02T00:19:14Z

This PR/issue depends on:

~~[Merged by Bors] - chore: golf using fun_prop #34441~~
~~[Merged by Bors] - chore(Archive): small golfs #34688~~
By Dependent Issues (🤖). Happy coding!

mathlib4-merge-conflict-bot · 2026-02-02T01:26:10Z

This pull request has conflicts, please merge master and resolve them.

The goal of this PR is to remove many explicit references to continuous(On)_const; to reduce the diff in leanprover-community#31607.

Use fun_prop more, and make indentation match mathlib style better. Extracted from leanprover-community#31607.

mathlib-merge-conflicts · 2026-02-17T06:16:01Z

This pull request has conflicts, please merge master and resolve them.

The goal of this PR is to remove many explicit references to continuous(On)_const; to reduce the diff in leanprover-community#31607.

Use fun_prop more, and make indentation match mathlib style better. Extracted from leanprover-community#31607.

The goal of this PR is to remove many explicit references to continuous(On)_const; to reduce the diff in leanprover-community#31607.

Use fun_prop more, and make indentation match mathlib style better. Extracted from leanprover-community#31607.

mathlib-merge-conflicts · 2026-03-08T14:56:01Z

This pull request has conflicts, please merge master and resolve them.

mathlib-merge-conflicts · 2026-03-13T20:37:31Z

This pull request has conflicts, please merge master and resolve them.

This issue was pre-existing, but has been exposed through leanprover-community#31607 where it caused test failures.

mathlib-merge-conflicts · 2026-03-20T16:26:02Z

This pull request has conflicts, please merge master and resolve them.

mathlib-merge-conflicts · 2026-03-23T20:05:24Z

This pull request has conflicts, please merge master and resolve them.

grunweg added the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Nov 13, 2025

j-loreaux reviewed Nov 15, 2025

View reviewed changes

ghost added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Nov 15, 2025

grunweg changed the title ~~chore: rename continuous{,On,At,Within}_const to ContinuousXXX.const`~~ chore: rename continuous{,On,At,Within}_const to ContinuousFoo.const` Nov 15, 2025

mathlib4-merge-conflict-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jan 7, 2026

grunweg removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jan 26, 2026

grunweg added a commit to grunweg/mathlib4 that referenced this pull request Jan 26, 2026

chore: golf using fun_prop

aa70da3

The goal of this PR is to remove many explicit references to continuous(On)_const; to reduce the diff in leanprover-community#31607

grunweg added a commit to grunweg/mathlib4 that referenced this pull request Jan 26, 2026

chore: golf using fun_prop

f58f238

The goal of this PR is to remove many explicit references to continuous(On)_const; to reduce the diff in leanprover-community#31607

grunweg mentioned this pull request Jan 26, 2026

[Merged by Bors] - chore: golf using fun_prop #34441

Closed

3 tasks

github-actions bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jan 27, 2026

mathlib-bors bot pushed a commit that referenced this pull request Jan 30, 2026

chore: golf using fun_prop (#34441)

409fcdc

The goal of this PR is to remove many explicit references to continuous(On)_const; to reduce the diff in #31607.

github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jan 30, 2026

mathlib4-merge-conflict-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 1, 2026

grunweg force-pushed the rename-continuousconst branch from 86fc9bd to 8501fa8 Compare February 1, 2026 16:13

github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 1, 2026

grunweg added a commit to grunweg/mathlib4 that referenced this pull request Feb 1, 2026

chore(Archive,Counterexamples): small golfs

3b68ac3

Use fun_prop more, and make indentation match mathlib style better. Extracted from leanprover-community#31607.

grunweg mentioned this pull request Feb 1, 2026

[Merged by Bors] - chore(Archive): small golfs #34688

Closed

mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Feb 1, 2026

mathlib-bors bot pushed a commit that referenced this pull request Feb 1, 2026

chore(Archive): small golfs (#34688)

3e8301e

Use fun_prop more, and make indentation match mathlib style better. Extracted from #31607.

mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Feb 2, 2026

mathlib4-merge-conflict-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 2, 2026

github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 2, 2026

Ruben-VandeVelde changed the title ~~chore: rename continuous{,On,At,Within}_const to ContinuousFoo.const`~~ chore: rename continuous{,On,At,Within}_const to ContinuousFoo.const Feb 2, 2026

YellPika pushed a commit to YellPika/mathlib4 that referenced this pull request Feb 3, 2026

chore: golf using fun_prop (leanprover-community#34441)

356bbf0

The goal of this PR is to remove many explicit references to continuous(On)_const; to reduce the diff in leanprover-community#31607.

github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 15, 2026

michaellee94 pushed a commit to michaellee94/mathlib4 that referenced this pull request Feb 15, 2026

chore(Archive): small golfs (leanprover-community#34688)

40e33c6

Use fun_prop more, and make indentation match mathlib style better. Extracted from leanprover-community#31607.

mathlib-merge-conflicts bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 17, 2026

Maldooor pushed a commit to Maldooor/mathlib4 that referenced this pull request Feb 25, 2026

chore: golf using fun_prop (leanprover-community#34441)

2b54b68

The goal of this PR is to remove many explicit references to continuous(On)_const; to reduce the diff in leanprover-community#31607.

Maldooor pushed a commit to Maldooor/mathlib4 that referenced this pull request Feb 25, 2026

chore(Archive): small golfs (leanprover-community#34688)

10a6c9e

Use fun_prop more, and make indentation match mathlib style better. Extracted from leanprover-community#31607.

pfaffelh pushed a commit to pfaffelh/mathlib4 that referenced this pull request Mar 2, 2026

chore: golf using fun_prop (leanprover-community#34441)

b2110e6

The goal of this PR is to remove many explicit references to continuous(On)_const; to reduce the diff in leanprover-community#31607.

pfaffelh pushed a commit to pfaffelh/mathlib4 that referenced this pull request Mar 2, 2026

chore(Archive): small golfs (leanprover-community#34688)

69a1f57

Use fun_prop more, and make indentation match mathlib style better. Extracted from leanprover-community#31607.

github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Mar 7, 2026

mathlib-merge-conflicts bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Mar 8, 2026

github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Mar 13, 2026

mathlib-merge-conflicts bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Mar 13, 2026

grunweg added a commit to grunweg/mathlib4 that referenced this pull request Mar 18, 2026

fix(Tactic/Continuity): mark Continuous.comp' as unsafe

0183fcd

This issue was pre-existing, but has been exposed through leanprover-community#31607 where it caused test failures.

grunweg mentioned this pull request Mar 18, 2026

fix(Tactic/Continuity): mark Continuous.comp' as unsafe #36806

Open

github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Mar 18, 2026

grunweg added 3 commits March 18, 2026 15:29

Rename and deprecations

f657303

Main PR

265d083

Make Continuous.comp' an unsafe rule; workaround a failure elsewhere

e7a1acf

grunweg force-pushed the rename-continuousconst branch from 1553504 to e7a1acf Compare March 18, 2026 14:31

More fixes

f429505

github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Mar 18, 2026

mathlib-merge-conflicts bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Mar 20, 2026

Merge branch 'master' into rename-continuousconst

7347cdf

github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Mar 21, 2026

mathlib-merge-conflicts bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Mar 23, 2026

	(ContinuousOn.const.mul hfc).sub (ContinuousOn.const.mul hgc)
	.sub (.mul .const hfc) (.mul .const hgc)

Conversation

grunweg commented Nov 13, 2025 • edited by Ruben-VandeVelde Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Nov 13, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 56e100aabd

Import changes for modified files

Declarations diff

Uh oh!

j-loreaux left a comment

Choose a reason for hiding this comment

Uh oh!

j-loreaux Nov 13, 2025

Choose a reason for hiding this comment

Uh oh!

mathlib-bors bot commented Nov 15, 2025

Uh oh!

mathlib4-merge-conflict-bot commented Jan 7, 2026

Uh oh!

mathlib4-merge-conflict-bot commented Feb 1, 2026

Uh oh!

mathlib4-dependent-issues-bot commented Feb 2, 2026

Uh oh!

mathlib4-merge-conflict-bot commented Feb 2, 2026

Uh oh!

mathlib-merge-conflicts bot commented Feb 17, 2026

Uh oh!

mathlib-merge-conflicts bot commented Mar 8, 2026

Uh oh!

mathlib-merge-conflicts bot commented Mar 13, 2026

Uh oh!

mathlib-merge-conflicts bot commented Mar 20, 2026

Uh oh!

mathlib-merge-conflicts bot commented Mar 23, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

grunweg commented Nov 13, 2025 •

edited by Ruben-VandeVelde

Loading

github-actions bot commented Nov 13, 2025 •

edited

Loading