Real.sqrt_eq_zero'
theorem Real.sqrt_eq_zero' : ∀ {x : ℝ}, x.sqrt = 0 ↔ x ≤ 0
This theorem states that for any real number `x`, the square root of `x`, as defined by the function `Real.sqrt`, is equal to zero if and only if `x` is less than or equal to zero. In other words, the square root of a real number is zero exactly when that number is non-positive.
More concisely: The square root of a real number is zero if and only if the number is non-positive.
|
Real.sqrt_pos_of_pos
theorem Real.sqrt_pos_of_pos : ∀ {x : ℝ}, 0 < x → 0 < x.sqrt
This theorem, referred to as an alias of the reverse direction of `Real.sqrt_pos`, states that for any real number `x`, if `x` is greater than 0, then the square root of `x` is also greater than 0. In mathematical terms, it can be written as: for all `x` in ℝ, if `x > 0` then `sqrt(x) > 0`.
More concisely: If a real number `x` is positive, then its square root is also positive. (i.e., `∀ x : ℝ, x > 0 → √x > 0`)
|
Real.sqrt_eq_zero_of_nonpos
theorem Real.sqrt_eq_zero_of_nonpos : ∀ {x : ℝ}, x ≤ 0 → x.sqrt = 0
The theorem `Real.sqrt_eq_zero_of_nonpos` asserts that for any real number `x`, if `x` is less than or equal to zero, then the square root of `x` is equal to zero. In mathematical notation, this can be stated as: for all \(x \in \mathbb{R}\), if \(x \leq 0\), then \(\sqrt{x} = 0\).
More concisely: For all real numbers x, if x ≤ 0 then √x = 0.
|
Real.sqrt_le_sqrt_iff
theorem Real.sqrt_le_sqrt_iff : ∀ {x y : ℝ}, 0 ≤ y → (x.sqrt ≤ y.sqrt ↔ x ≤ y)
This theorem describes a property of the square root function on real numbers. Specifically, it states that for any two real numbers `x` and `y`, with `y` being nonnegative, the square root of `x` is less than or equal to the square root of `y` if and only if `x` is less than or equal to `y`.
More concisely: For all real numbers x and y with y ≥ 0, √x ≤ √y if and only if x ≤ y.
|
Real.sqrt_one
theorem Real.sqrt_one : √1 = 1
This theorem states that the square root of 1 in the real numbers is equal to 1. In other words, when the `Real.sqrt` function is applied to the real number 1, the result is the real number 1. This corresponds to the well-known mathematical fact that $\sqrt{1} = 1$.
More concisely: The square root of 1 in the real numbers equals 1. (i.e., Real.sqrt 1 = 1)
|
Real.sqrt_lt'
theorem Real.sqrt_lt' : ∀ {x y : ℝ}, 0 < y → (x.sqrt < y ↔ x < y ^ 2)
The theorem `Real.sqrt_lt'` asserts that for any two real numbers `x` and `y`, if `y` is greater than zero, then the square root of `x` is less than `y` if and only if `x` is less than the square of `y`. In mathematical terms, this can be written as ∀ {x y : ℝ}, 0 < y → (sqrt(x) < y ↔ x < y^2).
More concisely: For any real numbers x and y with y > 0, sqrt(x) < y if and only if x < y^2.
|
NNReal.sq_sqrt
theorem NNReal.sq_sqrt : ∀ (x : NNReal), NNReal.sqrt x ^ 2 = x
This theorem states that for every nonnegative real number `x`, the square of the square root of `x` is equal to `x` itself. In mathematical terms, for all `x` in nonnegative real numbers, (√x)² = x. This is a formalization of the well-known property of the square root operation in real numbers.
More concisely: For all non-negative real numbers x, (√x)² = x.
|
Real.sqrt_nonneg
theorem Real.sqrt_nonneg : ∀ (x : ℝ), 0 ≤ x.sqrt
This theorem, `Real.sqrt_nonneg`, states that the square root of any real number is always nonnegative. In other words, for all real numbers `x`, the square root of `x` is greater than or equal to zero. This is expressed in mathematical terms as: ∀ (x : ℝ), 0 ≤ sqrt(x). Here, ℝ denotes the set of all real numbers. This result follows from the fact that the square root of a number is defined as a nonnegative number whose square is the original number.
More concisely: For all real numbers x, 0 ≤ sqrt(x).
|
Real.sqrt_pos
theorem Real.sqrt_pos : ∀ {x : ℝ}, 0 < x.sqrt ↔ 0 < x
The theorem `Real.sqrt_pos` states that for every real number `x`, the square root of `x` is positive if and only if `x` is positive. In other words, taking the square root of a positive real number results in a positive real number, and if the square root of a real number is positive, then the original number must have been positive.
More concisely: The square root of a positive real number is positive, and only positive real numbers have a positive square root.
|
Mathlib.Data.Real.Sqrt._auxLemma.13
theorem Mathlib.Data.Real.Sqrt._auxLemma.13 :
∀ {α : Type u} [inst : PartialOrder α] {a b : α}, (a = b) = (a ≤ b ∧ b ≤ a)
This theorem states that for any type `α` that has a partial order, given any two elements `a` and `b` of this type, `a` is equal to `b` if and only if `a` is less than or equal to `b` and `b` is less than or equal to `a`. In other words, two elements are equal in a partial order setting if they are mutually less than or equal to each other.
More concisely: In a partial order, two elements are equal if and only if they mutually satisfy the relationship of being less than or equal to each other.
|
Real.le_sqrt
theorem Real.le_sqrt : ∀ {x y : ℝ}, 0 ≤ x → 0 ≤ y → (x ≤ y.sqrt ↔ x ^ 2 ≤ y)
This theorem states that for any two real numbers `x` and `y`, given both `x` and `y` are non-negative, `x` is less than or equal to the square root of `y` if and only if the square of `x` is less than or equal to `y`. However, if you want to directly conclude that `x` is less than or equal to the square root of `y`, you should use the theorem `Real.le_sqrt_of_sq_le` instead. If `x` is strictly greater than 0, consider using the theorem `Real.le_sqrt'`.
More concisely: For any real numbers `x` and `y` with `x`, `y` ≥ 0, `x` ≤ √`y` if and only if `x²` ≤ `y`.
|
Real.continuous_sqrt
theorem Real.continuous_sqrt : Continuous fun x => x.sqrt
This theorem states that the square root function on real numbers is continuous. In other words, for every real number, small changes in the input lead to small changes in the output of the function, which in this case is the square root of the input. This is a fundamental property in calculus and real analysis.
More concisely: The square root function is a continuous function on the real numbers.
|
Real.real_sqrt_le_nat_sqrt_succ
theorem Real.real_sqrt_le_nat_sqrt_succ : ∀ {a : ℕ}, (↑a).sqrt ≤ ↑a.sqrt + 1
This theorem states that for every natural number `a`, the square root of `a` when treated as a real number is always less than or equal to the square root of `a` when treated as a natural number plus one. In mathematical terms, it translates to "∀a ∈ ℕ, sqrt(Real(a)) ≤ sqrt(Nat(a)) + 1".
More concisely: For all natural numbers `a`, the real square root of `a` is less than or equal to the natural square root of `a` plus one. (i.e., ∀a ∈ ℕ, sqrt(a) ≤ sqrt(Nat a) + 1)
|
Real.sqrt_mul_self
theorem Real.sqrt_mul_self : ∀ {x : ℝ}, 0 ≤ x → (x * x).sqrt = x
This theorem states that for any real number `x` that is greater than or equal to zero, the square root of the square of `x` is equal to `x`. In mathematical terms, for all real numbers `x` such that `x` is greater than or equal to zero, this is expressed as $\sqrt{x^2} = x$.
More concisely: For all real numbers `x` where `x` is non-negative, $\sqrt{x^2} = x$.
|
Real.sqrt_inv
theorem Real.sqrt_inv : ∀ (x : ℝ), x⁻¹.sqrt = x.sqrt⁻¹
This theorem states that for every real number x, the square root of the reciprocal of x is equal to the reciprocal of the square root of x. In mathematical notation, it's saying that for all x in the real numbers, √(1/x) = 1/√x. Note that the theorem applies only to real numbers.
More concisely: For all real numbers x, √(1/x) = 1/√x.
|
Real.sqrt_sq_eq_abs
theorem Real.sqrt_sq_eq_abs : ∀ (x : ℝ), (x ^ 2).sqrt = |x|
This theorem states that for every real number `x`, the square root of `x` squared is equal to the absolute value of `x`. In other words, taking the square root of the square of any real number will always yield the non-negative value of that number, effectively the absolute value. This is expressed mathematically as: ∀ (x : ℝ), √(x^2) = |x|.
More concisely: For all real numbers x, the square root of x squared equals its absolute value. That is, √(x^2) = |x|.
|
NNReal.sqrt_le_sqrt
theorem NNReal.sqrt_le_sqrt : ∀ {x y : NNReal}, NNReal.sqrt x ≤ NNReal.sqrt y ↔ x ≤ y
This theorem states that for any two nonnegative real numbers `x` and `y`, the square root of `x` is less than or equal to the square root of `y` if and only if `x` is less than or equal to `y`. In other words, the square root function on the nonnegative real numbers preserves the order of its inputs.
More concisely: For all non-negative real numbers x and y, x ≤ y if and only if √x ≤ √y.
|
Real.sqrt_zero
theorem Real.sqrt_zero : √0 = 0
This theorem states that the square root of zero in the set of real numbers is zero. In other words, when the `Real.sqrt` function is applied to 0, the output is also 0. This is in line with the mathematical property $\sqrt{0} = 0$.
More concisely: The square root of 0 in the real numbers is 0. (i.e., √0 = 0)
|
Real.coe_sqrt
theorem Real.coe_sqrt : ∀ {x : NNReal}, ↑(NNReal.sqrt x) = (↑x).sqrt
This theorem states that for every nonnegative real number `x`, the square root of `x` in the nonnegative real numbers (denoted as `NNReal.sqrt x`) when converted to a real number (through the operation `↑`) is equal to the square root of `x` in the real numbers (denoted as `Real.sqrt ↑x`). In mathematical language, this means that for every `x` in the set of nonnegative real numbers, `sqrt(x)` in the nonnegative real numbers and `sqrt(x)` in the real numbers are equivalent.
More concisely: For every non-negative real number `x`, `NNReal.sqrt x = Real.sqrt (↑x)`.
|
Real.le_sqrt_of_sq_le
theorem Real.le_sqrt_of_sq_le : ∀ {x y : ℝ}, x ^ 2 ≤ y → x ≤ y.sqrt
This theorem states that for any two real numbers `x` and `y`, if the square of `x` is less than or equal to `y`, then `x` is less than or equal to the square root of `y`. In mathematical terms, it would be expressed as: for all $x, y \in \mathbb{R}$, if $x^2 \leq y$, then $x \leq \sqrt{y}$. This theorem establishes a relationship between the square of a number and the square root of another number in the context of inequality.
More concisely: For all real numbers x and y, if x^2 ≤ y then x ≤ √y.
|
Real.nat_sqrt_le_real_sqrt
theorem Real.nat_sqrt_le_real_sqrt : ∀ {a : ℕ}, ↑a.sqrt ≤ (↑a).sqrt
This theorem states that for any natural number `a`, the natural square root of `a` is always less than or equal to the real square root of `a`. In mathematical terms, it means that for any natural number `a`, $\sqrt{a} \leq \sqrt{a}$ when the left hand side square root is calculated in the set of natural numbers and the right hand side square root is calculated in the set of real numbers.
More concisely: For any natural number `a`, the natural square root of `a` is less than or equal to the real square root of `a`. Mathematically, $\sqrt{a}_{\mathbb{N}} \leq \sqrt{a}_{\mathbb{R}}$.
|
Real.lt_sqrt
theorem Real.lt_sqrt : ∀ {x y : ℝ}, 0 ≤ x → (x < y.sqrt ↔ x ^ 2 < y)
This theorem states that for any two real numbers `x` and `y`, given that `x` is non-negative, then `x` is less than the square root of `y` if and only if the square of `x` is less than `y`. In mathematical notation, this is saying: for all real numbers `x` and `y` with `x` being greater than or equal to 0, `x` is less than `sqrt{y}` is equivalent to `x^2` being less than `y`.
More concisely: For any non-negative real numbers x and y, x < sqrt(y) if and only if x^2 < y.
|
Real.sqrt_le_left
theorem Real.sqrt_le_left : ∀ {x y : ℝ}, 0 ≤ y → (x.sqrt ≤ y ↔ x ≤ y ^ 2)
The theorem `Real.sqrt_le_left` states that for any two real numbers `x` and `y`, if `y` is greater or equal to zero, then the square root of `x` is less than or equal to `y` if and only if `x` is less than or equal to the square of `y`. In mathematical terms, for all real numbers x and y with y ≥ 0, √x ≤ y if and only if x ≤ y².
More concisely: For all real numbers x and y with y ≥ 0, √x ≤ y if and only if x ≤ y² (i.e., the square root of x is less than or equal to y if and only if x is less than or equal to the square of y).
|
Real.sqrt_sq
theorem Real.sqrt_sq : ∀ {x : ℝ}, 0 ≤ x → (x ^ 2).sqrt = x
The theorem `Real.sqrt_sq` states that for every real number `x`, given `x` is non-negative, the square root of the square of `x` is equal to `x` itself. In other words, if `x` is a non-negative real number, then applying the square root function to `x^2` returns `x`. In mathematical notation, this would be stated as: for all `x` in ℝ such that `x ≥ 0`, √(x^2) = x.
More concisely: For all non-negative real numbers `x`, $\sqrt{x^2} = x$.
|
Real.sqrt_le_sqrt
theorem Real.sqrt_le_sqrt : ∀ {x y : ℝ}, x ≤ y → x.sqrt ≤ y.sqrt
This theorem states that for all real numbers `x` and `y`, if `x` is less than or equal to `y`, then the square root of `x` is less than or equal to the square root of `y`. In other words, the function that sends a real number to its square root is a non-decreasing function.
More concisely: For all real numbers x and y, if x ≤ y then √x ≤ √y.
|
Real.sqrt_eq_iff_mul_self_eq
theorem Real.sqrt_eq_iff_mul_self_eq : ∀ {x y : ℝ}, 0 ≤ x → 0 ≤ y → (x.sqrt = y ↔ y * y = x)
This theorem is expressing a property of the square root function for real numbers. Specifically, it states that for any non-negative real numbers `x` and `y`, the square root of `x` is equal to `y` if and only if `y` squared is equal to `x`. In mathematical terms, given $x \geq 0$ and $y \geq 0$, $\sqrt{x} = y$ if and only if $y^2 = x$.
More concisely: The square root of a non-negative real number x is equal to y if and only if y^2 = x.
|
Real.sqrt_ne_zero'
theorem Real.sqrt_ne_zero' : ∀ {x : ℝ}, x.sqrt ≠ 0 ↔ 0 < x
This theorem states that for all real numbers 'x', the square root of 'x' (as defined by the function Real.sqrt) is not equal to zero if and only if 'x' is greater than zero. In other words, this theorem expresses a property of the square root function on the real numbers, stating that a number has a non-zero square root exactly when it is a positive number.
More concisely: For all real numbers x, x > 0 if and only if Real.sqrt x ≠ 0.
|
Real.abs_le_sqrt
theorem Real.abs_le_sqrt : ∀ {x y : ℝ}, x ^ 2 ≤ y → |x| ≤ y.sqrt
The theorem `Real.abs_le_sqrt` states that for all real numbers `x` and `y`, if the square of `x` is less than or equal to `y`, then the absolute value of `x` is less than or equal to the square root of `y`. In other words, given any two real numbers, if the square of the first is no greater than the second, the magnitude of the first number will not exceed the square root of the second number.
More concisely: For all real numbers x and y, if x^2 ≤ y then |x| ≤ √y.
|
Real.mul_self_sqrt
theorem Real.mul_self_sqrt : ∀ {x : ℝ}, 0 ≤ x → x.sqrt * x.sqrt = x
This theorem states that for any real number `x` that is greater than or equal to zero, the square root of `x` multiplied by itself equals `x`. In mathematical terms, it's saying that if `x` is a non-negative real number, then $\sqrt{x} \cdot \sqrt{x} = x$. This is the fundamental property of square roots applied to non-negative real numbers.
More concisely: For any non-negative real number `x`, $\sqrt{x} \cdot \sqrt{x} = x$.
|
Real.sqrt_mul_self_eq_abs
theorem Real.sqrt_mul_self_eq_abs : ∀ (x : ℝ), (x * x).sqrt = |x|
This theorem states that for any real number `x`, the square root of the square of `x` is equal to the absolute value of `x`. In mathematical terms, for all real numbers `x`, we have `sqrt(x^2) = |x|`.
More concisely: For all real numbers `x`, `sqrt(x^2) = |x|`.
|
Mathlib.Data.Real.Sqrt._auxLemma.17
theorem Mathlib.Data.Real.Sqrt._auxLemma.17 : ∀ {x : ℝ}, (0 < x.sqrt) = (0 < x)
This theorem states that for all real numbers `x`, the square root of `x` is positive if and only if `x` itself is positive. In other words, there is a direct correspondence between the positivity of a real number and the positivity of its square root, as calculated by the `Real.sqrt` function. Note that the `Real.sqrt` function returns 0 for negative inputs.
More concisely: For all real numbers `x`, `x` is positive if and only if the square root of `x` is positive.
|
NNReal.sqrt_pos_of_pos
theorem NNReal.sqrt_pos_of_pos : ∀ {x : NNReal}, 0 < x → 0 < NNReal.sqrt x
This theorem, called "NNReal.sqrt_pos_of_pos", states that for all nonnegative real numbers `x`, if `x` is greater than zero, then the square root of `x` (denoted by `NNReal.sqrt x`) is also greater than zero. In other words, the square root of any positive nonnegative real number is itself positive.
More concisely: For all nonnegative real numbers `x` greater than zero, `NNReal.sqrt x` is positive.
|
Mathlib.Data.Real.Sqrt._auxLemma.2
theorem Mathlib.Data.Real.Sqrt._auxLemma.2 : ∀ {x : NNReal}, (NNReal.sqrt x = 0) = (x = 0)
This theorem states that for all nonnegative real numbers `x`, the square root of `x` is zero if and only if `x` itself is zero. In other words, the only nonnegative real number whose square root is zero is zero itself. This is a fundamental property of the square root operation in the nonnegative real numbers.
More concisely: The square root of a nonnegative real number is zero if and only if the number itself is zero.
|
Real.sqrt_eq_iff_sq_eq
theorem Real.sqrt_eq_iff_sq_eq : ∀ {x y : ℝ}, 0 ≤ x → 0 ≤ y → (x.sqrt = y ↔ y ^ 2 = x)
This theorem, `Real.sqrt_eq_iff_sq_eq`, states that for any two real numbers `x` and `y`, both of which are non-negative, the square root of `x` equals `y` if and only if `y` squared equals `x`. In other words, it establishes a precise relationship between the square root function and the squaring operation on the real numbers, specifically on the non-negative part of the real line.
More concisely: For non-negative real numbers x and y, x = y^2 if and only if sqrt x = y.
|
Real.sqrt_mul
theorem Real.sqrt_mul : ∀ {x : ℝ}, 0 ≤ x → ∀ (y : ℝ), (x * y).sqrt = x.sqrt * y.sqrt
This theorem states that for any real number `x` that is greater than or equal to 0 and any real number `y`, the square root of the product of `x` and `y` is equal to the product of the square root of `x` and the square root of `y`. In terms of mathematical notation, this theorem is saying that for all $x, y \in \mathbb{R}$ with $x \geq 0$, we have $\sqrt{xy} = \sqrt{x} \cdot \sqrt{y}$.
More concisely: For any non-negative real numbers x and y, $\sqrt{xy} = \sqrt{x}\sqrt{y}$.
|
NNReal.sqrt_one
theorem NNReal.sqrt_one : NNReal.sqrt 1 = 1
This theorem states that the square root of 1, when considered within the set of nonnegative real numbers, is equal to 1. This is consistent with the usual mathematical understanding of square roots.
More concisely: The square root of 1, in the non-negative real numbers, equals 1.
|
Real.sq_sqrt
theorem Real.sq_sqrt : ∀ {x : ℝ}, 0 ≤ x → x.sqrt ^ 2 = x
This theorem states that for all real numbers `x`, if `x` is greater than or equal to zero, then the square of the square root of `x` is equal to `x`. In mathematical terms, for any real number `x` such that `x ≥ 0`, we have `sqrt(x)² = x`.
More concisely: For all real numbers `x` with `x ≥ 0`, `sqrt(x)² = x`.
|
Real.sqrt_lt_sqrt_iff
theorem Real.sqrt_lt_sqrt_iff : ∀ {x y : ℝ}, 0 ≤ x → (x.sqrt < y.sqrt ↔ x < y)
The theorem `Real.sqrt_lt_sqrt_iff` states that for any two real numbers `x` and `y`, if `x` is non-negative, then the square root of `x` is less than the square root of `y` if, and only if, `x` is less than `y`. This means that the ordering of the numbers `x` and `y` is preserved when taking their square roots, as long as `x` is non-negative.
More concisely: For any non-negative real numbers `x` and `y`, `sqrt x < sqrt y` if and only if `x < y`.
|