Require Import Coq.Reals.Reals.
Require Import Qreals.

Require Import Notations.Common.
Require Import Notations.Sets.

Notation "x ≠ y" := (x <> y) (at level 70) : type_scope.
Notation "x ≤ y" := (le x y) (at level 70, no associativity) : nat_scope.
Notation "x ≥ y" := (ge x y) (at level 70, no associativity) : nat_scope.
Notation "x ≤ y" := (x <= y)%R (at level 70, no associativity) : R_scope.
Notation "x ≥ y" := (x >= y)%R (at level 70, no associativity) : R_scope.

Open Scope nat_scope.
Open Scope R_scope.

Notation "'ℕ'" := (nat).
Notation "'ℤ'" := (Z).
Notation "'ℚ'" := (Q).
Notation "'ℝ'" := (R).

Coercion INR: nat >-> R.
Coercion IZR: Z >-> R.
Coercion Q2R: Q >-> R.

Open Scope subset_scope.

Definition converges_to (a : ℕ → ℝ) (c : ℝ) :=
  ∀ ε > 0, ∃ N1 ∈ ℕ, ∀ n ≥ N1, R_dist (a n) c < ε.

Notation "a ⟶ c" := (converges_to a c) (at level 20).

Definition cv_implies_cv_abs_to_l_abs := cv_cvabs.

Notation "| x |" := (Rabs x) (at level 65, x at next level, format "| x |").
Notation "｜ x - y ｜" := (R_dist x y) (at level 65, x at level 48, y at level 48, format "｜ x - y ｜") : R_scope.

Notation "'Σ' Cn 'equals' x" := (infinite_sum Cn x) (at level 50).

Definition finite_triangle_inequalty := sum_f_R0_triangle.

Notation "[ a , b ]" := (as_subset R (fun x => (a <= x <= b))): R_scope.
Notation "[ a , b )" := (as_subset R (fun x => (a <= x < b))): R_scope.
Notation "( a , b ]" := (as_subset R (fun x => (a < x <= b))): R_scope.
Notation "( a , b )" := (as_subset R (fun x => (a < x < b))): R_scope.

Close Scope subset_scope.
Close Scope nat_scope.
Close Scope R_scope.