Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Fix upper/lowercase in definitions #4354

Closed
3 tasks done
urkud opened this issue May 25, 2023 · 0 comments
Closed
3 tasks done

Fix upper/lowercase in definitions #4354

urkud opened this issue May 25, 2023 · 0 comments

Comments

@urkud
Copy link
Member

urkud commented May 25, 2023 •
edited

The following definitions are not aligned with, say, ULift/PLift.

  • Ulower -> ULower
  • Pcontinuous -> PContinuous
  • Dfinsupp -> DFinsupp
@urkud urkud changed the title Rename Ulower to ULower? Fix upper/lowercase in definitions May 25, 2023
urkud added a commit that referenced this issue May 28, 2023
@urkud
chore: rename Pcontinuous to PContinuous
610aa99 
ref #4354
@urkud urkud mentioned this issue May 28, 2023
Closed
urkud added a commit that referenced this issue May 28, 2023
@urkud
chore: rename Ulower to ULower
a668c2f 
ref #4354
@urkud urkud mentioned this issue May 28, 2023
Closed
bors bot pushed a commit that referenced this issue May 28, 2023
@urkud
chore: rename Pcontinuous to PContinuous (#4428)
3ff6ded 
ref #4354
bors bot pushed a commit that referenced this issue May 28, 2023
@urkud
chore: rename Ulower to ULower (#4430)
f93df69 
ref #4354
qawbecrdtey pushed a commit to qawbecrdtey/greedoid-mathlib4 that referenced this issue Jun 12, 2023
@urkud @qawbecrdtey
chore: rename Pcontinuous to PContinuous (leanprover-community#4428)
dde774a 
ref leanprover-community#4354
qawbecrdtey pushed a commit to qawbecrdtey/greedoid-mathlib4 that referenced this issue Jun 12, 2023
@urkud @qawbecrdtey
chore: rename Ulower to ULower (leanprover-community#4430)
80cd4c2 
ref leanprover-community#4354
urkud added a commit that referenced this issue Jul 11, 2023
@urkud
chore: rename Dfinsupp to DFinsupp
c3e2900 
See #4354

Should we use `FinSupp` and `DFinSupp`?
@urkud urkud mentioned this issue Jul 11, 2023
Closed
bors bot pushed a commit that referenced this issue Jul 11, 2023
@urkud
chore: rename Dfinsupp to DFinsupp (#5822)
91add9e 
See #4354
bors bot pushed a commit that referenced this issue Jul 12, 2023
@urkud
chore: rename Dfinsupp to DFinsupp (#5822)
268b7d4 
See #4354
@urkud urkud closed this as completed Jul 12, 2023
semorrison pushed a commit that referenced this issue Aug 14, 2023
@urkud @semorrison
chore: rename Dfinsupp to DFinsupp (#5822)
024515f 
See #4354
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@urkud