search

leanprover-community / mathlib

Lean 3's obsolete mathematical components library: please use mathlib4
https://leanprover-community.github.io/lean3
Apache License 2.0
1.66k stars 297 forks source link

refactor: change notation for interval integrals #19225

Closed urkud closed 2 weeks ago

urkud commented 1 year ago

Open in Gitpod

urkud commented 11 months ago

Changed to too-late because I failed to find a new notation that (a) will be accepted by the community; (b) works well both in Lean 3 and Lean 4.

urkud commented 2 weeks ago

Even if we'll decide to change notation in Lean 4, it no longer makes sense to change it in Lean 3 too.