Real.cauchy_add
theorem Real.cauchy_add : ∀ (a b : ℝ), (a + b).cauchy = a.cauchy + b.cauchy
This theorem states that for any two real numbers 'a' and 'b', the Cauchy sequence of the sum of 'a' and 'b' is equal to the sum of the Cauchy sequences of 'a' and 'b'. In other words, the operation of adding two real numbers commutes with the operation of taking their Cauchy sequences.
More concisely: For any real numbers a and b, the Cauchy sequences of a and b add componentwise to form the Cauchy sequence of a + b.
|
Real.mk_le
theorem Real.mk_le : ∀ {f g : CauSeq ℚ abs}, Real.mk f ≤ Real.mk g ↔ f ≤ g
The theorem `Real.mk_le` states that for any two Cauchy sequences of rational numbers, `f` and `g`, both evaluated by the absolute value function, the real number obtained from their equivalence classes through the `Real.mk` function is less than or equal to `g` if and only if the Cauchy sequence `f` is less than or equal to the Cauchy sequence `g`. In other words, the ≤ relation is preserved when moving from the Cauchy sequences of rational numbers to the real numbers.
More concisely: For any two Cauchy sequences of rational numbers `f` and `g`, `|f| ≤ |g|` in the real numbers if and only if `f(n) ≤ g(n)` for all natural numbers `n`.
|
Real.ext_cauchy
theorem Real.ext_cauchy : ∀ {x y : ℝ}, x.cauchy = y.cauchy → x = y
This theorem states that for any two real numbers `x` and `y`, if their Cauchy sequences are equal (i.e., `x.cauchy = y.cauchy`), then the real numbers themselves are also equal (`x = y`). This is a property linked to the construction of real numbers from Cauchy sequences of rational numbers, which ensures that distinct real numbers correspond to distinct Cauchy sequences.
More concisely: If two real numbers have equal Cauchy sequences, then they are equal.
|
Real.zero_lt_one
theorem Real.zero_lt_one : 0 < 1
This theorem is stating that zero is less than one in the set of real numbers. It is a fundamental truth in mathematics that forms the basis for many other mathematical concepts and operations. The theorem doesn't require any specific conditions or assumptions, it is universally valid.
More concisely: The theorem asserts that 0 < 1 in the set of real numbers.
|
Mathlib.Data.Real.Basic._auxLemma.1
theorem Mathlib.Data.Real.Basic._auxLemma.1 : ∀ {f g : CauSeq ℚ abs}, (Real.mk f < Real.mk g) = (f < g)
The theorem, `Mathlib.Data.Real.Basic._auxLemma.1`, states that for any two Cauchy sequences of rational numbers `f` and `g`, with respect to the absolute value function `abs`, the inequality `Real.mk f < Real.mk g` is equivalent to `f < g`. In other words, the inequality between two real numbers created from these Cauchy sequences (by taking their equivalence classes) mirrors the inequality between the original Cauchy sequences themselves.
More concisely: For any two Cauchy sequences of rational numbers `f` and `g`, `f < g` if and only if `|f| < |g|`, where `|.|` denotes the absolute value function.
|
Mathlib.Data.Real.Basic._auxLemma.8
theorem Mathlib.Data.Real.Basic._auxLemma.8 : ∀ {f g : CauSeq ℚ abs}, (Real.mk f ≤ Real.mk g) = (f ≤ g)
The theorem `Mathlib.Data.Real.Basic._auxLemma.8` states that for any two Cauchy sequences of rational numbers `f` and `g`, the real number created from the Cauchy sequence `f` is less than or equal to the real number created from the Cauchy sequence `g` if and only if the Cauchy sequence `f` is less than or equal to the Cauchy sequence `g`. In other words, the process of creating a real number from a Cauchy sequence of rational numbers preserves the order of the sequences.
More concisely: The real number obtained from a Cauchy sequence of rational numbers is less than or equal to the real number obtained from another Cauchy sequence if and only if the former sequence is less than or equal to the latter in terms of their convergence.
|
Real.ind_mk
theorem Real.ind_mk : ∀ {C : ℝ → Prop} (x : ℝ), (∀ (y : CauSeq ℚ abs), C (Real.mk y)) → C x
The theorem `Real.ind_mk` states that for any property `C` that holds for real numbers `ℝ`, and for any real number `x`, if this property `C` holds for all `Real.mk y`, where `y` is a Cauchy sequence of rationals `ℚ` with respect to the absolute value function `abs`, then the property `C` also holds for `x`. This can be interpreted as a form of induction over real numbers constructed from Cauchy sequences of rational numbers.
More concisely: If `C` is a property of real numbers and `C` holds for all Cauchy sequences of rationals converging to a real number `x`, then `C` holds for `x`.
|