Skip to content

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

Open
Chessing234 wants to merge 1 commit into
teorth:mainfrom
Chessing234:fix/exercise-1-3-8-ii-real-complex-simple
Open

fix: Exercise 1.3.8(ii) should be the real/complex simple function characterization#647
Chessing234 wants to merge 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:

theorem RealSimpleFunction.iff {d:ℕ} {f: EuclideanSpace' d → ℝ} :
  RealSimpleFunction f ↔ RealMeasurable f ∧ Finite (f '' Set.univ)

theorem ComplexSimpleFunction.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>
Sign up for free to 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.

1 participant