Skip to content

fix: Exercise 1.3.8(ii) should be the real/complex simple function characterization - #647

Merged
teorth merged 1 commit into
teorth:mainfrom
Chessing234:fix/exercise-1-3-8-ii-real-complex-simple
Aug 23, 2026
Merged

fix: Exercise 1.3.8(ii) should be the real/complex simple function characterization#647
teorth merged 1 commit into
teorth:mainfrom
Chessing234:fix/exercise-1-3-8-ii-real-complex-simple

Conversation

@Chessing234

Copy link
Copy Markdown
Contributor

Exercise 1.3.8 asks for the real- and complex-valued analogues of the unsigned results, and every other part in that block comes as a Real/Complex pair — (i) Continuous.RealMeasurable/Continuous.ComplexMeasurable, (iii) aeEqual, (iv) aeLimit, (v) comp_cts, (vi) add/sub/mul.

Part (ii), UnsignedSimpleFunction.iff', was instead a character-for-character copy of Exercise 1.3.5's unsigned statement (UnsignedSimpleFunction.iff, line 1752 of the same file). So the real/complex analogue was missing and 1.3.5 was posed twice.

Replaced with the two intended statements:

theoremRealSimpleFunction.iff {d:ℕ} {f: EuclideanSpace' d → ℝ} :
RealSimpleFunction f ↔ RealMeasurable f ∧ Finite (f '' Set.univ)
theoremComplexSimpleFunction.iff {d:ℕ} {f: EuclideanSpace' d → ℂ} :
ComplexSimpleFunction f ↔ ComplexMeasurable f ∧ Finite (f '' Set.univ)

Both bodies stay sorry. UnsignedSimpleFunction.iff' was not referenced anywhere in the repository, so nothing downstream changes.

Exercise 1.3.8 asks for the real- and complex-valued analogues of the
unsigned results, and every other part here comes as a Real/Complex pair.
Part (ii) was instead a verbatim copy of Exercise 1.3.5's unsigned
statement (UnsignedSimpleFunction.iff, earlier in this file), so the
real/complex analogue was missing and the same exercise was posed twice.
Replace it with the two intended statements. The duplicate name
UnsignedSimpleFunction.iff' was not referenced anywhere.
Signed-off-by: Taksh <takshkothari09@gmail.com>
@Chessing234
Chessing234force-pushed the fix/exercise-1-3-8-ii-real-complex-simple branch from beebc5f to 628d70eCompareAugust 12, 2026 16:45
@teorth
teorth merged commit 1cd4adf into teorth:mainAug 23, 2026
2 checks passed
Sign up for freeto join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants

@Chessing234@teorth