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

Add Theorems on Infimum Function Domains and Supporting Results #4616

Merged
merged 25 commits into from
Feb 2, 2025
Merged

Add Theorems on Infimum Function Domains and Supporting Results #4616

Changes from all commits
Commits
Show all changes
25 commits
Select commit Hold shift + click to select a range
a6c2c94
Remove unnecessary $d condition from theorems on sigma-measurable fun…
glacode Dec 15, 2024
6f57d69
Merge branch 'develop' of https://github.com/metamath/set.mm into MEA…
glacode Dec 16, 2024
dc89edd
Merge branch 'develop' of https://github.com/metamath/set.mm into MEA…
glacode Dec 20, 2024
331dab3
Add new pre-image theorems
glacode Dec 20, 2024
5407a9b
Merge branch 'develop' of https://github.com/metamath/set.mm into MEA…
glacode Dec 21, 2024
91bcaf1
Add new theorems involving the |`t operator.
glacode Dec 21, 2024
f12b394
Merge branch 'develop' of https://github.com/metamath/set.mm into MEA…
glacode Dec 26, 2024
bd0e6bb
Merge branch 'develop' of https://github.com/metamath/set.mm into MEA…
glacode Dec 30, 2024
2c889c6
Add theorems on domains of addition and multiplication in sigma-algebras
glacode Dec 30, 2024
d021013
Merge branch 'develop' of https://github.com/metamath/set.mm into MEA…
glacode Jan 2, 2025
4d73e93
Merge branch 'develop' of https://github.com/metamath/set.mm into MEA…
glacode Jan 5, 2025
a0b712f
Add new theorems related to restricted class abstraction, mappings, a…
glacode Jan 5, 2025
dcbc804
Merge branch 'develop' of https://github.com/metamath/set.mm into MEA…
glacode Jan 23, 2025
a5bd0f4
Merge branch 'develop' of https://github.com/metamath/set.mm into MEA…
glacode Jan 24, 2025
58b953d
~ rextru moved to main
glacode Jan 24, 2025
8d8756e
Merge branch 'develop' of https://github.com/metamath/set.mm into MEA…
glacode Jan 25, 2025
f068490
Updated the rextru comment. This update addresses Change Request #4599.
glacode Jan 25, 2025
56ee614
Merge branch 'develop' of https://github.com/metamath/set.mm into MEA…
glacode Jan 26, 2025
3452703
Add theorems on sup function domains and related results
glacode Jan 26, 2025
222b645
Merge branch 'develop' of https://github.com/metamath/set.mm into MEA…
glacode Jan 27, 2025
e51bcfc
Updated comments based on reviewers' feedback:
glacode Jan 27, 2025
c0aa5ae
Updated comments based on reviewers' feedback (part 2)
glacode Jan 27, 2025
723ce24
Merge branch 'develop' of https://github.com/metamath/set.mm into MEA…
glacode Jan 31, 2025
0270832
Merge branch 'develop' of https://github.com/metamath/set.mm into MEA…
glacode Feb 1, 2025
f5eeeca
Formalize Infimum Function Domain and Add Archimedean Helper Theorem
glacode Feb 1, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
154 changes: 154 additions & 0 deletions set.mm
View file
Open in desktop