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

Minimum and maximum on the lower, upper, and usual Dedekind real numbers #1335

Open

lowasser wants to merge 111 commits into UniMath:master from lowasser:min-max-lower-upper

+1,544 −0

Contributor

lowasser commented Feb 19, 2025

Depends on #1319.

lowasser added 30 commits

February 8, 2025 13:15


          Associativity of min and max

68ffc45


          Merge branch 'master' into min-max-associative

4ac4f7d


          Formatting

4a8b5c5


          Define lower Dedekind cuts/reals

6a9f837


          make pre-commit

ef39dd3


          Define upper Dedekind reals

59195c9


          make pre-commit

4233e28


          Rename things

6ad62d5


          Formatting

6bfb619


          Add new file

fd8f384


          Fix line length

fb0d5d3


          Merge branch 'lower-upper-dedekind' into lower-upper-rational-dedekind

efaf647


          Add rational upper reals

f21b948


          Progress

a3d3af9


          Merge branch 'lower-upper-rational-dedekind' into lower-upper-inequality

ba687cd


          Preservation of inequality

fb18a45


          Define normal Dedekind reals in terms of lower and upper cuts

0aa663c


          Merge branch 'lower-upper-inequality' into lower-upper-dedekind

1f9f502


          Start negation

7499c7c


          Inequality on upper reals

2185e18


          overhaul

f2da896


          make pre-commit

70f181c


          a -> an


          Merge branch 'master' into lower-upper-neg

e40e90b


          Rename some things

1b9d81b


          Merge branch 'master' into lower-upper-neg

d40a43a


          Some more theorems

f75209b


          Merge branch 'master' into lower-upper-neg

6d17056


          Finish gaps

098d4e8


          Progress

b3b72b2

fredrik-bakke reviewed

View reviewed changes

src/real-numbers/minimum-real-numbers.lagda.md Outdated Show resolved Hide resolved

fredrik-bakke reviewed

View reviewed changes

src/real-numbers/minimum-real-numbers.lagda.md Outdated Show resolved Hide resolved

fredrik-bakke reviewed

View reviewed changes

src/real-numbers/minimum-upper-dedekind-real-numbers.lagda.md Outdated Show resolved Hide resolved

fredrik-bakke reviewed

View reviewed changes

src/real-numbers/minimum-upper-dedekind-real-numbers.lagda.md Outdated Show resolved Hide resolved

fredrik-bakke reviewed

View reviewed changes

src/real-numbers/minimum-upper-dedekind-real-numbers.lagda.md Outdated Show resolved Hide resolved

fredrik-bakke reviewed

View reviewed changes

src/real-numbers/minimum-upper-dedekind-real-numbers.lagda.md Outdated Show resolved Hide resolved

fredrik-bakke reviewed

View reviewed changes

src/real-numbers/minimum-upper-dedekind-real-numbers.lagda.md Outdated Show resolved Hide resolved

fredrik-bakke reviewed

View reviewed changes

src/real-numbers/minimum-lower-dedekind-real-numbers.lagda.md Outdated Show resolved Hide resolved

fredrik-bakke reviewed

View reviewed changes

src/real-numbers/maximum-upper-dedekind-real-numbers.lagda.md Outdated Show resolved Hide resolved

fredrik-bakke reviewed

View reviewed changes

src/real-numbers/maximum-lower-dedekind-real-numbers.lagda.md Outdated Show resolved Hide resolved

fredrik-bakke approved these changes

View reviewed changes

Collaborator

fredrik-bakke left a comment

Very nice pull request!

Collaborator

fredrik-bakke commented Mar 22, 2025

If you could import the changes to minima and maxima of rational numbers from #1351, then this PR can be merged after you've addressed the comments here.

lowasser and others added 4 commits

March 22, 2025 10:19


          Apply suggestions from code review

69171a6

Co-authored-by: Fredrik Bakke <[email protected]>


          Merge branch 'master' into min-max-lower-upper

ba351a6


          Respond to review comments

8b3ad05


          make pre-commit

fad7de3

fredrik-bakke reviewed

View reviewed changes

src/real-numbers/minimum-upper-dedekind-real-numbers.lagda.md Outdated Show resolved Hide resolved

fredrik-bakke reviewed

View reviewed changes

src/real-numbers/maximum-real-numbers.lagda.md Outdated Show resolved Hide resolved

fredrik-bakke approved these changes

View reviewed changes

fredrik-bakke added 3 commits

March 23, 2025 10:53


          Update src/real-numbers/maximum-real-numbers.lagda.md

dd97d3b


          Update src/real-numbers/minimum-upper-dedekind-real-numbers.lagda.md


          Merge branch 'master' into min-max-lower-upper

2e2795e

fredrik-bakke enabled auto-merge (squash)

March 23, 2025 10:54

fredrik-bakke disabled auto-merge

March 23, 2025 10:55

Collaborator

fredrik-bakke commented Mar 23, 2025

Ah, I almost forgot to check the changes to maxima and minima of rational numbers. Please update those files with your changes from #1351, @lowasser.

lowasser added 2 commits

March 23, 2025 10:56


          Pull over changes to min/max on rationals

3507f55


          Merge remote-tracking branch 'origin/min-max-lower-upper' into min-ma…

e1e9c47

…x-lower-upper

Contributor Author

lowasser commented Mar 23, 2025

Done.

lowasser added 2 commits

March 23, 2025 17:54


          Merge branch 'master' into min-max-lower-upper

7d98d25


          Pull over more necessary changes

af942b4

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels