Real.Angle.sign_coe_pi_div_two
theorem Real.Angle.sign_coe_pi_div_two : (↑(Real.pi / 2)).sign = 1
The theorem `Real.Angle.sign_coe_pi_div_two` asserts that the sign of the angle π/2 (in radians), when represented as a real number, is 1. This is equivalent to stating that the sign of the sine of π/2 equals 1. In other words, it confirms that any angle strictly between 0 and π (both exclusive) has a sign of 1, and in this case the specific angle is π/2.
More concisely: The sign of the real number representation of π/2 radians is 1. Equivalently, the sine of π/2 is positive.
|
Real.Angle.toReal_le_pi
theorem Real.Angle.toReal_le_pi : ∀ (θ : Real.Angle), θ.toReal ≤ Real.pi
This theorem states that for any angle `θ` of type `Real.Angle`, when this angle is converted to a real number using the function `Real.Angle.toReal`, the resulting real number is less than or equal to π (`Real.pi`). In other words, the real number equivalent of any angle is always within the range from -π to π.
More concisely: For any angle `θ` of type `Real.Angle`, the value `Real.Angle.toReal θ` satisfies `-Real.pi ≤ Real.Angle.toReal θ ≤ Real.pi`.
|
Real.Angle.neg_pi_div_two_ne_zero
theorem Real.Angle.neg_pi_div_two_ne_zero : ↑(-Real.pi / 2) ≠ 0
This theorem states that the negative half of the real number π, when coerced (converted) to an angle, is not equal to zero. In mathematical terms, −π/2 is not zero when we consider it as an angle. This theorem is important as it helps in ensuring the uniqueness and non-zero nature of angle values in mathematical proofs and computations.
More concisely: The theorem asserts that the angle representation of the negative half of π is not equal to 0. That is, -π/2 ≠ 0.
|
Real.Angle.cos_coe
theorem Real.Angle.cos_coe : ∀ (x : ℝ), (↑x).cos = x.cos
This theorem states that for every real number `x`, the cosine of the `Real.Angle` corresponding to `x` (obtained by considering `x` as an angle in radians) is equal to the value of the real cosine function at `x`. Formally, if `↑x` denotes the conversion of `x` from a real number to a `Real.Angle`, then `Real.Angle.cos ↑x = Real.cos x` for all real numbers `x`.
More concisely: For every real number `x`, the cosine of the angle `x` in radians is equal to the cosine of `x` as a real number, i.e., `Real.Angle.cos (Real.pi * x / 180) = Real.cos x`.
|
Real.Angle.induction_on
theorem Real.Angle.induction_on : ∀ {p : Real.Angle → Prop} (θ : Real.Angle), (∀ (x : ℝ), p ↑x) → p θ
This theorem provides an induction principle for the type `Real.Angle`. It states that for any property `p` that applies to angles (`Real.Angle`), if that property holds for all real numbers when they are considered as angles, then it must also hold for any arbitrary angle `θ`. This theorem is useful when you want to prove something about all angles (`Real.Angle`) and you already know how to prove it for all real numbers (`ℝ`). You would use it with the `induction θ using Real.Angle.induction_on` tactic in Lean.
More concisely: If a property holds for all real numbers when considered as angles, then it holds for any arbitrary angle. (Induction principle for `Real.Angle` type in Lean)
|
Real.Angle.coe_add
theorem Real.Angle.coe_add : ∀ (x y : ℝ), ↑(x + y) = ↑x + ↑y
This theorem, `Real.Angle.coe_add`, states that for any two real numbers `x` and `y`, the angle of their sum is equal to the sum of their angles. In other words, it asserts that the operation of taking the angle is compatible with addition in the real numbers. Written in mathematical notation, this would be: for all real numbers `x` and `y`, the angle of `(x + y)` is equal to the angle of `x` plus the angle of `y`.
More concisely: For all real numbers x and y, the angle of (x + y) is equal to the sum of the angles of x and y.
|
Real.Angle.toReal_coe_eq_self_iff_mem_Ioc
theorem Real.Angle.toReal_coe_eq_self_iff_mem_Ioc : ∀ {θ : ℝ}, (↑θ).toReal = θ ↔ θ ∈ Set.Ioc (-Real.pi) Real.pi := by
sorry
This theorem states that for any real number 'θ', the function 'Real.Angle.toReal' applied to 'θ' mapped into the Real.Angle set, equals 'θ' itself if and only if 'θ' belongs to the interval '(-π, π]' (in terms of the real numbers). Here, the interval '(-π, π]' signifies a left-open and right-closed interval, meaning that it includes all real numbers strictly greater than '-π' and less than or equal to 'π'.
More concisely: For any real number 'θ', the function 'Real.Angle.toReal' equals 'θ' if and only if 'θ' belongs to the interval '(-π, π]'.
|
Real.Angle.sign_eq_of_continuousOn
theorem Real.Angle.sign_eq_of_continuousOn :
∀ {α : Type u_1} [inst : TopologicalSpace α] {f : α → Real.Angle} {s : Set α} {x y : α},
IsConnected s →
ContinuousOn f s → (∀ z ∈ s, f z ≠ 0 ∧ f z ≠ ↑Real.pi) → x ∈ s → y ∈ s → (f y).sign = (f x).sign
The theorem `Real.Angle.sign_eq_of_continuousOn` states that for any set `s` of some type `α` with a topological structure, if `s` is connected and has a function `f` mapping from `α` to Real Angles that is continuous on `s`, and this function `f` never takes the values `0` or `π` for any element in `s`, then for any two elements `x` and `y` in `s`, the signs of the values of the function `f` at `x` and `y` are the same. This implies that all function values on a connected set under these conditions have the same sign.
More concisely: If `s` is a connected set with topology, `f` is a continuous function from `s` to Real Angles on `s` with no values of `0` or `π`, then for all `x, y` in `s`, the signs of `f x` and `f y` are equal.
|
Real.Angle.toReal_injective
theorem Real.Angle.toReal_injective : Function.Injective Real.Angle.toReal
The theorem `Real.Angle.toReal_injective` states that the function `Real.Angle.toReal`, which converts a `Real.Angle` to a real number in the interval `(-π, π)`, is injective. This means that if two angles are mapped to the same real number by this function, then those two angles were the same to start with. In other words, no two different angles will be mapped to the same real number by the `Real.Angle.toReal` function.
More concisely: The function `Real.Angle.toReal` maps distinct `Real.Angle` values to distinct real numbers in the interval `(-π, π)`.
|
Real.Angle.tan_coe
theorem Real.Angle.tan_coe : ∀ (x : ℝ), (↑x).tan = x.tan
This theorem states that for every real number `x`, the tangent of the angle corresponding to `x` (when `x` is interpreted as a real angle) is equal to the real tangent of `x`. In mathematical terms, for all `x` in real numbers, `tan(↑x)` (where `↑x` stands for the angle corresponding to `x`) equals `tan(x)`.
More concisely: For all real numbers x, the tangent of the angle with radian measure x is equal to the real value of the tangent function of x.
|
Real.Angle.pi_ne_zero
theorem Real.Angle.pi_ne_zero : ↑Real.pi ≠ 0
This theorem states that the real number representation of the mathematical constant pi (π), as defined in Lean 4, is not equal to zero. In other words, it guarantees that the value of pi, approximately equal to 3.14159265, cannot be zero, consistent with its mathematical definition.
More concisely: The theorem asserts that the value of Pi in Lean 4 is not equal to zero.
|
Real.Angle.toReal_zero
theorem Real.Angle.toReal_zero : Real.Angle.toReal 0 = 0
This theorem states that when the function `Real.Angle.toReal` is applied to zero, it returns zero. In other words, the image of zero under the conversion from a real angle to a real number in the interval `(-π, π)` is zero itself.
More concisely: The theorem asserts that `Real.Angle.toReal` applied to zero angle equals zero in the real numbers.
|
Real.Angle.pi_div_two_ne_zero
theorem Real.Angle.pi_div_two_ne_zero : ↑(Real.pi / 2) ≠ 0
This theorem states that the value of π divided by 2, when mapped from the real numbers to the complex numbers, is not equal to zero. In other words, half of π does not map to the complex zero.
More concisely: The theorem asserts that π/2 ≠ 0 in the complex numbers.
|
Real.Angle.toReal_pi
theorem Real.Angle.toReal_pi : (↑Real.pi).toReal = Real.pi
This theorem states that the real number representation of the `Real.Angle` corresponding to the mathematical constant π (pi), when converted back to a real number using the `Real.Angle.toReal` function, still remains as the original real number π. In other words, converting π from a real number to a `Real.Angle` and then back to a real number doesn't change the value, it still stays as π.
More concisely: The real number representation of the `Real.Angle` constant π, obtained via `Real.Angle.toReal`, is equal to the original real number value of π.
|
Real.Angle.coe_sub
theorem Real.Angle.coe_sub : ∀ (x y : ℝ), ↑(x - y) = ↑x - ↑y
This theorem states that for any two real numbers `x` and `y`, the angle of their difference is equal to the difference of their angles. In other words, converting the difference of two real numbers into an angle (represented by `↑(x - y)`) is the same as first converting the numbers into angles and then subtracting them (represented by `↑x - ↑y`).
More concisely: For any real numbers x and y, ↑(x - y) = ↑x - ↑y.
|
Real.Angle.coe_toReal
theorem Real.Angle.coe_toReal : ∀ (θ : Real.Angle), ↑θ.toReal = θ
This theorem, `Real.Angle.coe_toReal`, states that for every angle `θ` of type `Real.Angle`, the operation of converting `θ` to a real number in the interval `Ioc (-π) π` via the function `Real.Angle.toReal`, and then lifting it back to the `Real.Angle` type through the coercion operation (`↑`), yields the original angle `θ`. In simpler terms, this theorem asserts that the conversion between `Real.Angle` and real numbers via `Real.Angle.toReal` and back is lossless - you end up with the exact same angle you started with.
More concisely: The conversion of a real number in the interval `(-π, π)` to an `Real.Angle` type and back using `Real.Angle.toReal` and coercion is a lossless operation. In mathematical notation, given `θ : Real.Angle` such that `Real.Angle.toReal θ ∈ (-π, π)`, we have `θ = ↑(Real.Angle.toReal θ)`.
|
Real.Angle.sign_antiperiodic
theorem Real.Angle.sign_antiperiodic : Function.Antiperiodic Real.Angle.sign ↑Real.pi
This theorem states that the sign function for a real angle is antiperiodic with an antiperiod of pi (π). In other words, for any real angle x, the sign of the angle at x + π is the negative of the sign at x. This is consistent with the trigonometric characteristics of sine function, which underlies the definition of the sign of a real angle.
More concisely: The sign function of a real angle is antiperiodic with an antiperiod of pi, i.e., sign(x + pi) = -sign(x) for all real x.
|
Real.Angle.sin_neg
theorem Real.Angle.sin_neg : ∀ (θ : Real.Angle), (-θ).sin = -θ.sin
This theorem states that for any angle `θ` of the type `Real.Angle`, the sine of the negative of `θ` is equal to the negative of the sine of `θ`. In mathematical terms, this is saying that $\sin(-θ) = -\sin(θ)$ for any real angle `θ`. This is essentially the property of the sine function being an odd function in trigonometry.
More concisely: The sine function is an odd function, that is, $\sin(-θ) = -\sin(θ)$ for all real angles `θ`.
|
Real.Angle.sign_neg
theorem Real.Angle.sign_neg : ∀ (θ : Real.Angle), (-θ).sign = -θ.sign
This theorem states that for every real angle `θ`, the sign of the negative of that angle is the negative of the sign of the angle. In other words, if we negate an angle and then take the sign, it's the same as taking the sign of the original angle and then negating it. This is equivalent to the mathematical statement that for all real angles θ, sign(-θ) = -sign(θ), where sign refers to the definition provided which determines the sign based on the sine of the angle.
More concisely: For all real angles θ, sign(-θ) = -sign(θ).
|
Real.Angle.neg_coe_pi
theorem Real.Angle.neg_coe_pi : -↑Real.pi = ↑Real.pi
The theorem `Real.Angle.neg_coe_pi` states that the negative of the real number representation of pi (`-↑Real.pi`) is equal to the real number representation of pi (`↑Real.pi`). In other words, it's saying that pi and negative pi are equal when considered as real numbers. It should be noted that this equality is not true in the ordinary real number field but is accurate in the context of angles, where adding or subtracting any multiple of `2π` to an angle gives a co-terminal angle, meaning pi and negative pi represent the same angle.
More concisely: The theorem `Real.Angle.neg_coe_pi` asserts that `-↑Real.pi = ↑Real.pi` in the context of real numbers representing angles.
|
Real.Angle.two_nsmul_eq_iff
theorem Real.Angle.two_nsmul_eq_iff : ∀ {ψ θ : Real.Angle}, 2 • ψ = 2 • θ ↔ ψ = θ ∨ ψ = θ + ↑Real.pi
This theorem states that for any two angles `ψ` and `θ`, the condition of doubling `ψ` to get the same result as doubling `θ` (expressed as `2 • ψ = 2 • θ`) holds if and only if `ψ` is either equal to `θ` or `ψ` equals `θ` plus π. Here, angles are defined in the type `Real.Angle`, which comprises real numbers modulo `2 * π`, and π is defined as twice a zero of the cosine function in the interval [1,2].
More concisely: For angles `ψ` and `θ` in the real modulo `2π`, `2ψ = 2θ` if and only if `ψ` is equal to `θ` or `ψ` is `θ` plus `π`.
|
Real.Angle.neg_pi_lt_toReal
theorem Real.Angle.neg_pi_lt_toReal : ∀ (θ : Real.Angle), -Real.pi < θ.toReal
The theorem `Real.Angle.neg_pi_lt_toReal` asserts that for any angle `θ` represented as a Real.Angle type, the real number representation of `θ` (obtained using the `Real.Angle.toReal` function) is always greater than negative pi (`-π`). In other words, the conversion of any angle to a real number results in a value that lies in the interval `(-π, +∞)`.
More concisely: For any angle θ represented as a Real.Angle type in Lean 4, the real number representation of θ (obtained through `Real.Angle.toReal`) is strictly greater than -π.
|
Real.Angle.toReal_neg_iff_sign_neg
theorem Real.Angle.toReal_neg_iff_sign_neg : ∀ {θ : Real.Angle}, θ.toReal < 0 ↔ θ.sign = -1
This theorem states that for any real angle 'θ', the real number representation of 'θ' will be less than zero if and only if the sign of 'θ' is -1. The sign of a real angle is defined as the sign of the sine of the angle: it's 0 if the angle is 0 or π, 1 if the angle is strictly between 0 and π, and -1 if the angle is strictly between -π and 0. Therefore, according to this theorem, a negative real representation of a real angle implies that its sine is negative, i.e., the angle is strictly between -π and 0.
More concisely: The real representation of a real angle is negative if and only if the angle's sine is negative, i.e., the angle is strictly between -π and 0.
|
Real.Angle.sign_ne_zero_iff
theorem Real.Angle.sign_ne_zero_iff : ∀ {θ : Real.Angle}, θ.sign ≠ 0 ↔ θ ≠ 0 ∧ θ ≠ ↑Real.pi
This theorem states that the sign of an angle θ in the real plane (represented as a `Real.Angle`) is non-zero if and only if the angle θ is not equal to 0 and θ is not equal to π (represented as `Real.pi`). This is based on the earlier definition where the sign of an angle is 0 if the angle is either 0 or π, and non-zero otherwise.
More concisely: The sign of a real angle θ is non-zero if and only if θ ≠ 0 and θ ≠ π.
|
Real.Angle.toReal_inj
theorem Real.Angle.toReal_inj : ∀ {θ ψ : Real.Angle}, θ.toReal = ψ.toReal ↔ θ = ψ
The theorem `Real.Angle.toReal_inj` states that for any two angles `θ` and `ψ` represented as `Real.Angle`, the function `Real.Angle.toReal` is injective; this means that `θ` and `ψ` are equal if and only if their images under `Real.Angle.toReal` are equal. In other words, converting `θ` and `ψ` to real numbers in the interval `(-π, π]` yields the same number if and only if `θ` and `ψ` are the same angle.
More concisely: The function `Real.Angle.toReal` maps distinct angles to distinct real numbers in the interval `(-π, π]`.
|
Real.Angle.toReal_coe_eq_self_iff
theorem Real.Angle.toReal_coe_eq_self_iff : ∀ {θ : ℝ}, (↑θ).toReal = θ ↔ -Real.pi < θ ∧ θ ≤ Real.pi
This theorem states that for any real number `θ`, the function `Real.Angle.toReal` applied to the coersion of `θ` to a `Real.Angle` returns `θ` if and only if `θ` is strictly greater than negative pi (`-π`) and less than or equal to pi (`π`). In other words, converting a real number to a Real.Angle and then back to a real number yields the original number only if the original number lies within the interval `(-π, π]`.
More concisely: The theorem asserts that for any real number `θ`, `Real.Angle.toReal (toReal θ) = θ` if and only if `θ` is in the interval `(-π, π]`.
|
Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle._auxLemma.9
theorem Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle._auxLemma.9 :
∀ {M : Type u} [inst : AddMonoid M] (a : M), a + a = 2 • a
This theorem states that for any type `M` that has an `AddMonoid` instance, for any element `a` of type `M`, the sum of `a` and `a` is equal to two times `a`. In mathematical terms, it means that for any element in an additive monoid, doubling the element through addition is the same as scalar multiplication by 2.
More concisely: For any additive monoid `M` and element `a` in `M`, the operation of adding `a` to itself twice is equivalent to multiplying `a` by 2. (Or, more concisely: `2 * a = a + a` for all `a` in an additive monoid.)
|
Real.Angle.angle_eq_iff_two_pi_dvd_sub
theorem Real.Angle.angle_eq_iff_two_pi_dvd_sub : ∀ {ψ θ : ℝ}, ↑θ = ↑ψ ↔ ∃ k, θ - ψ = 2 * Real.pi * ↑k
This theorem states that for any two real numbers, `θ` and `ψ`, `θ` is congruent to `ψ` modulo `2π` if and only if there exists an integer `k` such that the difference `θ - ψ` is equal to `2π` multiplied by `k`. In other words, two angles are equivalent if their difference is a multiple of `2π`, reflecting the periodicity of the trigonometric functions.
More concisely: Two real numbers `θ` and `ψ` are congruent modulo `2π` if and only if their difference `θ - ψ` is equal to an integer multiple of `2π`.
|
Real.Angle.sin_toReal
theorem Real.Angle.sin_toReal : ∀ (θ : Real.Angle), θ.toReal.sin = θ.sin
This theorem states that for every angle `θ` of type `Real.Angle`, the real sine of its corresponding real number (which lies in the interval (-π, π)) equals to the sine of the angle `θ` itself. In other words, the function `Real.sin` applied to the real number equivalent of the angle (calculated using `Real.Angle.toReal`) gives the same result as the function `Real.Angle.sin` applied to the angle directly.
More concisely: For every angle `θ`, the real value `Real.sin (Real.Angle.toReal θ)` equals `Real.Angle.sin θ`.
|
Real.Angle.coe_zero
theorem Real.Angle.coe_zero : ↑0 = 0
This theorem, named `Real.Angle.coe_zero`, states that the real number coercion of zero is zero. Essentially, when zero is considered as a real number, it remains zero.
More concisely: The real number coercion of 0 is equal to 0. (Or, the conversion of 0 from the type of integers to the type of real numbers results in the same number, 0.)
|
Real.Angle.sin_coe
theorem Real.Angle.sin_coe : ∀ (x : ℝ), (↑x).sin = x.sin
This theorem states that, for any real number `x`, the sine of the angle formed by `x` (when `x` is interpreted as a real angle), is equal to the real sine of `x`. In other words, the function `Real.Angle.sin` applied to the co-domain of `x` (that is, `↑x`) results in the same value as the `Real.sin` function applied directly to `x`. This establishes a consistency between the sine function applied to real numbers and the sine of the angle formed by real numbers.
More concisely: For any real number x, the sine of the angle x is equal to the real value of the sine function applied to x. (Or, in mathematical notation: ∀x: ℝ, sin(ang x) = sin x)
|
Real.Angle.coe_two_pi
theorem Real.Angle.coe_two_pi : ↑(2 * Real.pi) = 0
This theorem states that when you take the number π (which is approximately 3.14159265...), multiply it by 2, and then convert it into the type of angle measurement used in Lean (`Real.Angle`), you get 0. This is consistent with the standard interpretation in mathematics, where an angle of 2π radians equates to a full rotation, or 0 in the modular arithmetic of angles.
More concisely: The theorem asserts that 2π in radians is equivalent to 0 degrees in Lean's `Real.Angle` type.
|
Real.Angle.coe_nsmul
theorem Real.Angle.coe_nsmul : ∀ (n : ℕ) (x : ℝ), ↑(n • x) = n • ↑x
This theorem states that for any natural number `n` and any real number `x`, the real number representation of `n` multiplied by `x` is equal to `n` multiplied by the real number representation of `x`. In other words, it asserts that the process of scalar multiplication can be interchanged with the process of converting between natural numbers and real numbers. This is a property of the embedding of natural numbers into the reals.
More concisely: For any natural number `n` and real number `x`, the conversion of `n` to a real number and multiplication by `x` is equal to multiplication by `x` of the real number representation of `n`.
|
Real.Angle.sign_eq_zero_iff
theorem Real.Angle.sign_eq_zero_iff : ∀ {θ : Real.Angle}, θ.sign = 0 ↔ θ = 0 ∨ θ = ↑Real.pi
The theorem `Real.Angle.sign_eq_zero_iff` states that for any angle `θ` of type `Real.Angle`, the sign of the angle `θ` is zero if and only if the angle `θ` is either zero or equal to pi (`π`). Here, pi is defined as a real number `Real.pi` and the sign of an angle is determined by `Real.Angle.sign` function, which is based on the sign of the sine of the angle.
More concisely: The sign of a real angle is zero if and only if the angle is either 0 or equal to pi. (In Lean 4, this is expressed as `Real.Angle.sign θ = 0 ↔ θ = 0 or θ = Real.pi`)
|
Real.Angle.coe_neg
theorem Real.Angle.coe_neg : ∀ (x : ℝ), ↑(-x) = -↑x
This theorem states that for all real numbers `x`, the angle of the negative of `x` is equal to the negative of the angle of `x`. Here, `↑` denotes the function that maps real numbers to angles. Essentially, this theorem captures the idea that negating a real number and then converting it to an angle is the same as first converting the real number to an angle and then negating it.
More concisely: For all real numbers x, the angle of the negative x is equal to the negative of the angle of x. (or equivalently, the angle of -x = -angle x)
|