kdrag.theories.real.lim_algebra

Algebra of real sequence limits.

Theorem	Statement
real.lim_algebra.abs_add	∀x y : ℝ, |x + y| ≤ |x| + |y|
real.lim_algebra.abs_div	∀x y : ℝ, y ≠ 0 → |x / y| = |x| / |y|
real.lim_algebra.abs_mul	∀x y : ℝ, |x * y| = |x| * |y|
real.lim_algebra.abs_neg	∀x : ℝ, |-x| = |x|
real.lim_algebra.abs_pos	∀x : ℝ, |x| ≥ 0
real.lim_algebra.abs_pos_iff	∀x : ℝ, (|x| > 0) = (x ≠ 0)
real.lim_algebra.abs_triangle	∀x y z : ℝ, |x - y| ≤ |x - z| + |z - y|
real.lim_algebra.div_decomp	∀u v w z : ℝ,   v ≠ 0 ∧ z ≠ 0 →   u / v + -1 * (w / z) = (u - w) / v + w * ((z - v) / (v * z))
real.lim_algebra.has_lim_add	∀a b : ℤ → ℝ, x y : ℝ,   has_lim(a, x) → has_lim(b, y) → has_lim(a + b, x + y)
real.lim_algebra.has_lim_div	∀a b : ℤ → ℝ, x y : ℝ,   has_lim(a, x) →   has_lim(b, y) → y ≠ 0 → has_lim(a / b, x / y)
real.lim_algebra.has_lim_mul	∀a b : ℤ → ℝ, x y : ℝ,   has_lim(a, x) → has_lim(b, y) → has_lim(a * b, x * y)
real.lim_algebra.has_lim_smul	∀a : ℤ → ℝ, x c : ℝ,   has_lim(a, x) → has_lim(RSeq.smul(c, a), c * x)
real.lim_algebra.lim_of_nonneg_seq	∀a : ℤ → ℝ, y : ℝ,   has_lim(a, y) → (∀n : ℤ, n ≥ 0 → a[n] ≥ 0) → y ≥ 0