real_analysis.math

[\reals]
Defines: R
Documented:
. written: "\mathbb{R}"
. called: "reals"
------------------------------------------
Id: "aecb5b16-2e9a-4602-b489-1b81a5cdca0f"


[\real]
Describes: x
specifies: 'x [.in.]: \reals'
Documented:
. called: "real"
------------------------------------------
Id: "81d27721-4b8e-4d6d-9b49-23b3b426ca4f"


[\positive.real]
Describes: x
Documented:
. called: "positive real"
------------------------------------------
Id: "8f0ed422-74b2-4bbb-873f-9e272ad4bd6f"


[\real.sqrt(x)]
Defines: f(x) := y
means: 'f is \function:on{\reals}:to{\reals}'
expresses:
. 'y > 0'
. 'y^2 = x'
------------------------------------------
Id: "19f87c85-964d-417a-b91e-a2f600259d75"


[\uniqueness.of.positive.nth.root]
Theorem:
given: x, n
where:
. 'x is \real'
. 'n is \positive.natural'
then:
. existsUnique: y
  where: 'y is \real'
  suchThat:
  . 'y > 0'
  . 'y^n = x'
------------------------------------------
Id: "33e40ee0-5046-4535-9a09-747f254a6c40"


[\real.nth.root(x)]
Defines: f(x) := y
when: 'n is \positive.natural'
means: 'f is \function:on{\reals}:to{\reals}'
expresses:
. 'y > 0'
. 'y^n = x'
Justified:
. by: "\[uniqueness.of.positive.nth.root]"
------------------------------------------
Id: "e94770b4-62b0-4acd-8cf0-c18a26d89217"


[\real.square(x)]
Defines: f(x)
means: 'f is \function:on{\reals}:to{\reals}'
expresses: 'f(x) := x^2'
------------------------------------------
Id: "bd82c6f5-13de-4b95-a9fd-6ff4cda2a7ea"


[\archimedian.property]
Theorem:
given: a, b
where: 'a, b is \positive.real'
then:
. exists: n
  where: 'n is \natural'
  suchThat: 'a*n > b'
------------------------------------------
Id: "cc499976-02ec-49b2-836c-11695ba79ca7"