Real.arccos_neg
theorem Real.arccos_neg : ∀ (x : ℝ), (-x).arccos = Real.pi - x.arccos
The theorem `Real.arccos_neg` states that for any real number `x`, the arccosine of the negation of `x` is equivalent to the difference of the number π and the arccosine of `x`. In more mathematical terms, it states that for all real numbers `x`, the equality `arccos(-x) = π - arccos(x)` holds true. This property is a fundamental identity in trigonometry.
More concisely: For all real numbers x, arccos(-x) = π - arccos(x).
|
Real.arcsin_eq_of_sin_eq
theorem Real.arcsin_eq_of_sin_eq : ∀ {x y : ℝ}, x.sin = y → x ∈ Set.Icc (-(Real.pi / 2)) (Real.pi / 2) → y.arcsin = x
The theorem states that for any real numbers `x` and `y`, if `y` is the sine of `x` and `x` lies in the closed interval from negative half pi to half pi (i.e., `-π / 2 ≤ x ≤ π / 2`), then the arcsine of `y` is `x`. In other words, it establishes the reversibility of the sine function within its principal domain of `[-π/2, π/2]` under the arcsine function.
More concisely: For any real numbers `x` and `y`, if `y = sin(x)` and `-π/2 ≤ x ≤ π/2`, then `x = arcsin(y)`.
|
Real.arcsin_le_iff_le_sin
theorem Real.arcsin_le_iff_le_sin :
∀ {x y : ℝ}, x ∈ Set.Icc (-1) 1 → y ∈ Set.Icc (-(Real.pi / 2)) (Real.pi / 2) → (x.arcsin ≤ y ↔ x ≤ y.sin) := by
sorry
The theorem `Real.arcsin_le_iff_le_sin` states that for any real numbers 'x' and 'y', where 'x' is in the closed interval between -1 and 1 and 'y' is in the closed interval between -π/2 and π/2, the arcsine of 'x' is less than or equal to 'y' if and only if 'x' is less than or equal to the sine of 'y'.
More concisely: For real numbers x in [-1, 1] and y in [-π/2, π/2], arcsin(x) ≤ y if and only if x ≤ sin(y).
|
Real.arcsin_one
theorem Real.arcsin_one : Real.arcsin 1 = Real.pi / 2
This theorem states that the arcsine of 1 is equal to π/2. In other words, the angle whose sine is 1, when measured in radians within the interval from -π/2 to π/2, as defined by `Real.arcsin`, is π/2.
More concisely: The theorem asserts that `Real.arcsin 1 = π/2`.
|
Real.arccos_cos
theorem Real.arccos_cos : ∀ {x : ℝ}, 0 ≤ x → x ≤ Real.pi → x.cos.arccos = x
This theorem states that for all real numbers `x` in the range from 0 to π (inclusive), the arc cosine of the cosine of `x` equals `x`. It essentially describes the property of the `arccos` function being the inverse of the `cos` function within the specified range. In mathematical terms, if 0 ≤ x ≤ π, then arccos(cos(x)) = x.
More concisely: For all real numbers `x` in the range [0, π], the arc cosine of the cosine of `x` equals `x`: `arccos(cos x) = x`.
|
Real.arcsin_zero
theorem Real.arcsin_zero : Real.arcsin 0 = 0
This theorem states that the arcsine of 0 is 0. In mathematical terms, this would be written as arcsin(0) = 0. Arcsine is the inverse function of sine, and this theorem is saying that when you apply the arcsine function to 0, you get a result of 0.
More concisely: The theorem asserts that the value of the inverse sine function is zero for input zero: arcsin(0) = 0.
|
Real.arcsin_nonneg
theorem Real.arcsin_nonneg : ∀ {x : ℝ}, 0 ≤ x.arcsin ↔ 0 ≤ x
The theorem `Real.arcsin_nonneg` states that for any real number `x`, the arcsine of `x` is nonnegative if and only if `x` itself is nonnegative. In other words, the arcsine function preserves the nonnegativity of real numbers.
More concisely: For any real number `x`, `0 ≤ x` if and only if `0 ≤ arcsin x`.
|
Real.arcsin.proof_2
theorem Real.arcsin.proof_2 : -1 ≤ 1
This theorem establishes the basic numerical fact that negative one is less than or equal to positive one in the domain of real numbers. In mathematical notation, it simply is stating that $-1 \leq 1$. While this may seem obvious, in formal theorem proving, even these sorts of basic facts need to be established as theorems.
More concisely: The theorem asserts that $-1 \leq 1$ in the realm of real numbers.
|
Real.sin_arcsin
theorem Real.sin_arcsin : ∀ {x : ℝ}, -1 ≤ x → x ≤ 1 → x.arcsin.sin = x
The theorem `Real.sin_arcsin` is stating that for all real numbers x such that x is within the interval [-1, 1], the sine of the arcsine of x is equal to x. In other words, if you take the arcsine (the inverse sine function) of any real number between -1 and 1, and then take the sine of the result, you will get back your original number. This encapsulates the property of the inverse trigonometric function - the fact that applying a function and its inverse will yield the original value.
More concisely: For all real x in the interval [-1, 1], sin(arcsin(x)) = x.
|
Real.arcsin_of_le_neg_one
theorem Real.arcsin_of_le_neg_one : ∀ {x : ℝ}, x ≤ -1 → x.arcsin = -(Real.pi / 2)
This theorem states that for any real number `x`, if `x` is less than or equal to `-1`, then the arcsine of `x` (represented by `Real.arcsin x` in Lean) is equal to negative half of pi (denoted by `-(Real.pi / 2)`). In mathematical notation, this is equivalent to the statement that for all x in ℝ, if x ≤ -1, then arcsin(x) = -π/2.
More concisely: For any real number `x` below `-1`, the arcsine function `Real.arcsin x` equals `-(Real.pi / 2)`.
|
Real.continuous_arccos
theorem Real.continuous_arccos : Continuous Real.arccos
This theorem states that the inverse of the cosine function, `arccos`, is continuous. In mathematical terms, it means that for every point in its domain, the function `arccos` does not have any jumps, breaks, or holes. It ensures that for any given small change in the input (x), there will be a correspondingly small change in the output (`arccos x`).
More concisely: The function `arccos` is a continuous function on its domain.
|
Real.le_arcsin_iff_sin_le'
theorem Real.le_arcsin_iff_sin_le' :
∀ {x y : ℝ}, x ∈ Set.Ioc (-(Real.pi / 2)) (Real.pi / 2) → (x ≤ y.arcsin ↔ x.sin ≤ y)
This theorem states that for all real numbers `x` and `y`, where `x` is in the set of real numbers that fall in the interval from negative pi over 2 (exclusive of this boundary) to pi over 2 (inclusive of this boundary), the inequality `x` being less than or equal to the arcsine of `y` is equivalent to the sine of `x` being less than or equal to `y`. This theorem thus links the arcsine and sine functions through this inequality relationship on a specific interval for `x`.
More concisely: For real numbers `x` in (-π/2, π/2] and `y`, the inequality `x ≤ arcsin(y)` is equivalent to `sin(x) ≤ y`.
|
Real.strictMonoOn_arcsin
theorem Real.strictMonoOn_arcsin : StrictMonoOn Real.arcsin (Set.Icc (-1) 1)
The theorem `Real.strictMonoOn_arcsin` states that the inverse sine function, `arcsin`, is strictly monotonic on the interval from -1 to 1, inclusive. In other words, if `a` and `b` are any two different real numbers in the closed interval from -1 to 1 (i.e., `-1 ≤ a, b ≤ 1`), and `a < b`, then the `arcsin` of `a` is less than the `arcsin` of `b` (i.e., `arcsin(a) < arcsin(b)`).
More concisely: The inverse sine function is strictly increasing on the interval [-1, 1].
|
Real.neg_pi_div_two_lt_arcsin
theorem Real.neg_pi_div_two_lt_arcsin : ∀ {x : ℝ}, -(Real.pi / 2) < x.arcsin ↔ -1 < x
The theorem states that for all real numbers `x`, the negative half of Pi is less than the arcsin of `x` if and only if `-1` is less than `x`. In other words, the arcsin function returns values greater than `-π/2` if and only if the input `x` is greater than `-1`. This theorem sets the lower boundary for the input to the arcsin function in relation to the output range of `-π/2` to `π/2`.
More concisely: For all real numbers x, arcsin(x) < -π/2 if and only if x < -1.
|
Real.arcsin_sin
theorem Real.arcsin_sin : ∀ {x : ℝ}, -(Real.pi / 2) ≤ x → x ≤ Real.pi / 2 → x.sin.arcsin = x
This theorem states that for all real numbers `x` that lie within the interval from `-π / 2` to `π / 2` (inclusive), the arcsine of the sine of `x` is equal to `x`. Essentially, this says that the function `arcsin(sin(x))` acts as the identity for `x` in the stated interval. Specifically, for real numbers `x` such that `-π / 2 ≤ x ≤ π / 2`, `arcsin(sin(x))` returns `x`.
More concisely: For all real numbers `x` in the interval `[-π/2, π/2]`, the function `arcsin(sin(x))` equals `x`.
|
Real.arcsin_of_one_le
theorem Real.arcsin_of_one_le : ∀ {x : ℝ}, 1 ≤ x → x.arcsin = Real.pi / 2
The theorem `Real.arcsin_of_one_le` states that for all real numbers `x`, if `x` is greater than or equal to 1, then the inverse of the sine function of `x`, also known as `arcsin(x)`, is equal to π/2. This means `arcsin(x)` defaults to π/2 for `x` in the interval [1, ∞).
More concisely: For all real numbers `x` with `x ≥ 1`, `arcsin x = π/2`.
|
Real.arcsin_neg
theorem Real.arcsin_neg : ∀ (x : ℝ), (-x).arcsin = -x.arcsin
This theorem states that for every real number 'x', the arcsine of negative 'x' is equal to the negative of the arcsine of 'x'. In other words, the arcsine function has symmetry about the origin, which means flipping the input sign also flips the output sign.
More concisely: For all real numbers x, arcsin(-x) = -arcsin(x).
|
Real.continuous_arcsin
theorem Real.continuous_arcsin : Continuous Real.arcsin
The theorem `Real.continuous_arcsin` states that the function `Real.arcsin`, which is defined as the inverse of the sine function, is continuous. In mathematical terms, for any real number `x`, the limit as `y` approaches `x` of `Real.arcsin(y)` is equal to `Real.arcsin(x)`. This applies for all real numbers within the domain of `Real.arcsin`, which is from `-π / 2` to `π / 2`, inclusive.
More concisely: The function `Real.arcsin` is continuous on the interval `[-π/2, π/2]`.
|
Real.neg_pi_div_two_le_arcsin
theorem Real.neg_pi_div_two_le_arcsin : ∀ (x : ℝ), -(Real.pi / 2) ≤ x.arcsin
This theorem states that for every real number 'x', the value of the arcsine function at 'x' is always greater than or equal to negative pi divided by 2. This is essentially stating the lower bound of the range of the arcsine function in the real number system.
More concisely: For all real numbers x, arcsin x ≥ -π/2.
|
Real.arcsin_le_iff_le_sin'
theorem Real.arcsin_le_iff_le_sin' :
∀ {x y : ℝ}, y ∈ Set.Ico (-(Real.pi / 2)) (Real.pi / 2) → (x.arcsin ≤ y ↔ x ≤ y.sin)
This theorem states that for all real numbers `x` and `y`, if `y` is in the left-closed right-open interval from negative half pi to half pi (i.e., `-π / 2 ≤ y < π / 2`), then the arcsine of `x` is less than or equal to `y` if and only if `x` is less than or equal to the sine of `y`. In other words, it is establishing a relation between the arcsine and sine functions within the specified interval for `y` in terms of inequality.
More concisely: For all real numbers x and y with -π/2 ≤ y < π/2, arcsin(x) ≤ y if and only if x ≤ sin(y).
|
Real.arcsin_lt_pi_div_two
theorem Real.arcsin_lt_pi_div_two : ∀ {x : ℝ}, x.arcsin < Real.pi / 2 ↔ x < 1
This theorem states that for any real number `x`, the arcsine of `x` is less than half of pi if and only if `x` is less than 1. In mathematical terms, it's saying that for all `x` in the set of real numbers ℝ, `arcsin(x) < π/2` is equivalent to `x < 1`.
More concisely: The theorem asserts that for all real numbers `x`, `arcsin(x) < π/2` if and only if `x < 1`.
|
Real.sin_arcsin'
theorem Real.sin_arcsin' : ∀ {x : ℝ}, x ∈ Set.Icc (-1) 1 → x.arcsin.sin = x
This theorem states that for all real numbers `x` within the interval from -1 to 1, inclusive, the sine of the arcsine of `x` equals `x`. In other words, when `x` is in the interval [-1, 1], the `sin` and `arcsin` functions are inverses of each other. This theorem is essentially capturing the mathematical concept that $sin(arcsin(x)) = x$ for $x$ in the range $[-1, 1]$.
More concisely: For all real numbers `x` in the interval [-1, 1], sin(arcsin(x)) = x holds.
|
Real.arcsin_mem_Icc
theorem Real.arcsin_mem_Icc : ∀ (x : ℝ), x.arcsin ∈ Set.Icc (-(Real.pi / 2)) (Real.pi / 2)
This theorem states that for any real number `x`, the arcsine of `x` (as defined in Lean 4 using `Real.arcsin`) always falls within the closed interval from negative half pi to half pi, i.e., $-\frac{\pi}{2} \leq \arcsin(x) \leq \frac{\pi}{2}$. This reflects the standard mathematical property of the arcsine function, which only returns values in this range.
More concisely: For all real numbers x, $-{\pi}/{2} \leq \arcsin(x) \leq {\pi}/{2}$.
|
Real.arccos_zero
theorem Real.arccos_zero : Real.arccos 0 = Real.pi / 2
The theorem `Real.arccos_zero` states that the arccosine of zero equals to half of the mathematical constant pi. In other words, it denotes that the inverse of the cosine function, when applied to zero, results in π/2. The arccosine function is defined in the set of real numbers, and π is defined as twice the zero of the cosine function in the interval [1,2].
More concisely: The arccosine of 0 is equal to π/2.
|
Real.arcsin_le_pi_div_two
theorem Real.arcsin_le_pi_div_two : ∀ (x : ℝ), x.arcsin ≤ Real.pi / 2
This theorem states that for any real number `x`, the arcsine of `x` (denoted as `Real.arcsin x` in Lean 4) is less than or equal to half of the mathematical constant π (denoted as `Real.pi / 2` in Lean 4). The arcsine function in Lean 4 returns values in the range `-π / 2 ≤ arcsin x ≤ π / 2`, and this theorem confirms the upper bound of this range.
More concisely: For all real numbers x, the arcsine of x (arcsin x) is bounded above by π/2.
|