Real.cos_arctan_pos
theorem Real.cos_arctan_pos : ∀ (x : ℝ), 0 < x.arctan.cos
The theorem `Real.cos_arctan_pos` states that the cosine of the arctangent of any real number is always positive. In other words, for all real numbers `x`, the value of `cos(arctan(x))` is greater than zero.
More concisely: For all real numbers x, cos(arctan(x)) > 0.
|
Real.tan_arctan
theorem Real.tan_arctan : ∀ (x : ℝ), x.arctan.tan = x
This theorem states that for all real numbers `x`, the tangent of the arctangent of `x` equals `x`. In other words, the tangent function and the arctangent function are inverses of each other when composed in the order tan(arctan(x)). This is similar to the familiar trigonometric identity that the tangent of the arctangent of a number returns the original number.
More concisely: The theorem asserts that for all real numbers `x`, the function composition tan(arctan(x)) equals `x`.
|
Real.arctan_tan
theorem Real.arctan_tan : ∀ {x : ℝ}, -(Real.pi / 2) < x → x < Real.pi / 2 → x.tan.arctan = x
This theorem, `Real.arctan_tan`, states that for all real numbers `x`, if `x` is strictly greater than negative half of pi and strictly less than half of pi, then the arctangent of the tangent of `x` is equal to `x`. In other words, for any `x` in the open interval (-π/2, π/2), the inverse tangent (or arctangent) function is the inverse of the tangent function.
More concisely: For all real numbers `x` in the open interval `(-π/2, π/2)`, `arctan(tan(x)) = x`.
|
Real.arctan_eq_arcsin
theorem Real.arctan_eq_arcsin : ∀ (x : ℝ), x.arctan = (x / (1 + x ^ 2).sqrt).arcsin
The theorem `Real.arctan_eq_arcsin` states that for all real numbers `x`, the arctangent of `x` is equal to the arcsine of the expression `x / sqrt(1 + x^2)`. Here, `sqrt` refers to the square root of a real number. This theorem provides a relationship between the arctangent and arcsine functions, revealing them to be related through a particular expression involving the input `x`.
More concisely: For all real numbers x, arctan x = arcsin (x / √(1 + x²)).
|
Real.arctan_zero
theorem Real.arctan_zero : Real.arctan 0 = 0
The theorem `Real.arctan_zero` states that the arctangent of zero is zero. In other words, when the real number zero is passed as an argument to the arctangent function (`Real.arctan`), the result is the real number zero. This is consistent with the mathematical property that the inverse tangent of zero is zero.
More concisely: The arctangent function evaluates to 0 for the input of 0. (Real.arctan 0 = 0)
|
Real.arctan_mem_Ioo
theorem Real.arctan_mem_Ioo : ∀ (x : ℝ), x.arctan ∈ Set.Ioo (-(Real.pi / 2)) (Real.pi / 2)
The theorem `Real.arctan_mem_Ioo` states that for any real number `x`, the inverse tangent of `x`, denoted as `Real.arctan x`, is always within the open interval `( -π/2 , π/2 )`. Here, `Set.Ioo` refers to a left-open right-open interval, meaning both ends of the range are not included. Therefore, the theorem asserts that the value of `arctan(x)` is strictly greater than `-π/2` and strictly less than `π/2` for any real `x`.
More concisely: The theorem `Real.arctan_mem_Ioo` asserts that for all real numbers `x`, `Real.arctan x` lies in the open interval `(-\pi/2, \pi/2)`.
|
Real.continuous_arctan
theorem Real.continuous_arctan : Continuous Real.arctan
This theorem states that the arctan function, which is the inverse of the tangent function, is continuous. In the context of real numbers, a function is continuous if the function does not have any jumps, breaks, or holes. Specifically, the Real.arctan function takes a real number input and returns a real number output, and this output changes smoothly as the input changes. The theorem implies that for any value in the domain of the function, a small change in the input will result in a small change in the output; there are no sudden or abrupt changes in the value of the function.
More concisely: The arctan function is a continuous real-valued function.
|
Real.arctan_lt_pi_div_two
theorem Real.arctan_lt_pi_div_two : ∀ (x : ℝ), x.arctan < Real.pi / 2
This theorem states that for any real number `x`, the arctan of `x` is less than π/2. The arctan function is the inverse of the tangent function and returns values in the range `-π/2 < arctan x < π/2`. The constant π, approximately 3.14159265, is defined as twice a zero of the cosine function in the interval [1,2].
More concisely: For all real numbers x, the value of arctan x is less than π/2.
|