Add new theorems related to restricted class abstraction, mappings, and measurable functions #4537
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
- Reduced constraints by replacing them with 'effectively not free' hypotheses. - Improves theorem usability and simplifies certain dependencies.
This commit includes: - Theorems specific to sigma-algebras about the |`t operator. - Theorems specific to topologies about the |`t operator. - General theorems about the |`t operator. Additionally, variations of existing theorems have been added: - Deduction versions (e.g., ~ inopnd). - 'Effectively not free' versions (e.g., ~ ss2rabdf).
This commit introduces four theorems related to the domains of function addition and multiplication within the context of sigma-algebras: Theorems adddmmbl and adddmmbl2: If two functions have domains in a sigma-algebra, the domain of their addition also belongs to the sigma-algebra. These theorems correspond to the first statement of Proposition 121H from [Fremlin1], p. 39. The assumption of sigma-measurability for the functions, as in the original text, is not required here. Theorems muldmmbl and muldmmbl2: Similarly, if two functions have domains in a sigma-algebra, the domain of their multiplication also belongs to the sigma-algebra. These theorems correspond to the second statement of Proposition 121H from [Fremlin1], p. 39, again without requiring sigma-measurability. This commit also adds four missing full stops in previously committed comments.
…nd measurable functions This commit introduces some new theorems to set.mm, including contributions related to subclass relationships, domains of mappings, functionality, and sigma-algebra measurable functions. These include: Subclass of a restricted class abstraction (deduction form): ssrabdf Domain of the mapping operation (deduction form): dmmpt1 Functionality of the mapping operation: fmptff Function value and codomain relationship: fvmptelcdmf Mapping operation with bound-variable hypothesis: fmptdff Function measurability in sigma-algebras: smffmptf: Demonstrates measurability as a function. smfdmmblpimne: Predomain of 'all but one' of measurable functions in sigma-algebras. smfdivdmmbl: Domain of a division of measurable functions in sigma-algebras. smfdivdmmbl2: Variant of smfdivdmmbl using function notation. smfpimne: Preimage of reals different from a given value in a subspace sigma-algebra. smfpimne2: Variant of smfpimne with the extended real assumption relaxed to existence.
|
wlammen
reviewed
Jan 6, 2025
| smfdmmblpimne.6 $e |- ( ph -> ( x e. A |-> B ) e. ( SMblFn ` S ) ) $. | ||
| smfdmmblpimne.7 $e |- ( ph -> C e. RR ) $. | ||
| smfdmmblpimne.8 $e |- D = { x e. A | B =/= C } $. | ||
| $( If a measurable function w.r.t. to a sigma-algebra has domain in the |
There was a problem hiding this comment.
If the domain of a measurable function ... is in the sigma-algebra ,...
There was a problem hiding this comment.
Hi @wlammen,
Fremlin's book (which I'm following) states:
"I seek to deal with functions which are not defined on the whole of the space X under consideration. I believe that there are compelling reasons for facing up to such functions at an early stage."
This perspective is crucial, especially when addressing the limits of functions, which can have "bizarre" domains—even when the initial functions are defined on the entire sigma-algebra. For more details, see ~smflim.
Additionally, ~smfmbfcex provides examples of measurable functions with non-measurable domains (e.g., take
X to be the Vitali set). My definition includes a broader class of measurable functions compared to MblFn.
There was a problem hiding this comment.
I did not expect this. So OK then.
wlammen
approved these changes
Jan 6, 2025
icecream17
approved these changes
Jan 6, 2025
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This commit introduces some new theorems to set.mm, including contributions related to subclass relationships, domains of mappings, functionality, and sigma-algebra measurable functions. These include:
General Contributions:
ssrabdfdmmpt1fmptfffvmptelcdmffmptdffMeasurable Functions and Sigma-Algebras:
smffmptfandsmffmptsmfdmmblpimnesmfpimnesmfpimne2smfdivdmmblsmfdivdmmbl2