From Coq Require Import ZArith Reals ssreflect.

Require Import Rcomplements Rbar Hierarchy Compactness Lim_seq.

Local Tactic Notation "intuition" := (intuition auto with arith zarith real).

Definition is_lim (f : R → R) (x l : Rbar) :=
  filterlim f (Rbar_locally' x) (Rbar_locally l).

Definition is_lim' (f : R → R) (x l : Rbar) :=
  match l with
    | Finite l ⇒
      ∀ eps : posreal, Rbar_locally' x (fun y ⇒ Rabs (f y - l) < eps)
    | p_infty ⇒ ∀ M : R, Rbar_locally' x (fun y ⇒ M < f y)
    | m_infty ⇒ ∀ M : R, Rbar_locally' x (fun y ⇒ f y < M)
  end.
Definition ex_lim (f : R → R) (x : Rbar) := ∃ l : Rbar, is_lim f x l.
Definition ex_finite_lim (f : R → R) (x : Rbar) := ∃ l : R, is_lim f x l.
Definition Lim (f : R → R) (x : Rbar) := Lim_seq (fun n ⇒ f (Rbar_loc_seq x n)).

Lemma is_lim_spec :
  ∀ f x l,
  is_lim' f x l ↔ is_lim f x l.

Lemma is_lim_Reals_0 (f : R → R) (x l : R) :
  is_lim f x l → limit1_in f (fun y ⇒ y ≠ x) l x.
Lemma is_lim_Reals_1 (f : R → R) (x l : R) :
  limit1_in f (fun y ⇒ y ≠ x) l x → is_lim f x l.
Lemma is_lim_Reals (f : R → R) (x l : R) :
  is_lim f x l ↔ limit1_in f (fun y ⇒ y ≠ x) l x.

Lemma is_lim_comp' :
  ∀ {T} {F} {FF : @Filter T F} (f : T → R) (g : R → R) (x l : Rbar),
  filterlim f F (Rbar_locally x) → is_lim g x l →
  F (fun y ⇒ Finite (f y) ≠ x) →
  filterlim (fun y ⇒ g (f y)) F (Rbar_locally l).

Lemma is_lim_comp_seq (f : R → R) (u : nat → R) (x l : Rbar) :
  is_lim f x l →
  eventually (fun n ⇒ Finite (u n) ≠ x) →
  is_lim_seq u x → is_lim_seq (fun n ⇒ f (u n)) l.

Lemma is_lim_unique (f : R → R) (x l : Rbar) :
  is_lim f x l → Lim f x = l.
Lemma Lim_correct (f : R → R) (x : Rbar) :
  ex_lim f x → is_lim f x (Lim f x).

Lemma ex_finite_lim_correct (f : R → R) (x : Rbar) :
  ex_finite_lim f x ↔ ex_lim f x ∧ is_finite (Lim f x).
Lemma Lim_correct' (f : R → R) (x : Rbar) :
  ex_finite_lim f x → is_lim f x (real (Lim f x)).

Lemma is_lim_ext_loc (f g : R → R) (x l : Rbar) :
  Rbar_locally' x (fun y ⇒ f y = g y)
  → is_lim f x l → is_lim g x l.
Lemma ex_lim_ext_loc (f g : R → R) (x : Rbar) :
  Rbar_locally' x (fun y ⇒ f y = g y)
  → ex_lim f x → ex_lim g x.
Lemma Lim_ext_loc (f g : R → R) (x : Rbar) :
  Rbar_locally' x (fun y ⇒ f y = g y)
  → Lim g x = Lim f x.

Lemma is_lim_ext (f g : R → R) (x l : Rbar) :
  (∀ y, f y = g y)
  → is_lim f x l → is_lim g x l.
Lemma ex_lim_ext (f g : R → R) (x : Rbar) :
  (∀ y, f y = g y)
  → ex_lim f x → ex_lim g x.
Lemma Lim_ext (f g : R → R) (x : Rbar) :
  (∀ y, f y = g y)
  → Lim g x = Lim f x.

Lemma is_lim_comp (f g : R → R) (x k l : Rbar) :
  is_lim f l k → is_lim g x l → Rbar_locally' x (fun y ⇒ Finite (g y) ≠ l)
    → is_lim (fun x ⇒ f (g x)) x k.
Lemma ex_lim_comp (f g : R → R) (x : Rbar) :
  ex_lim f (Lim g x) → ex_lim g x → Rbar_locally' x (fun y ⇒ Finite (g y) ≠ Lim g x)
    → ex_lim (fun x ⇒ f (g x)) x.
Lemma Lim_comp (f g : R → R) (x : Rbar) :
  ex_lim f (Lim g x) → ex_lim g x → Rbar_locally' x (fun y ⇒ Finite (g y) ≠ Lim g x)
    → Lim (fun x ⇒ f (g x)) x = Lim f (Lim g x).

Lemma is_lim_id (x : Rbar) :
  is_lim (fun y ⇒ y) x x.
Lemma ex_lim_id (x : Rbar) :
  ex_lim (fun y ⇒ y) x.
Lemma Lim_id (x : Rbar) :
  Lim (fun y ⇒ y) x = x.

Lemma is_lim_const (a : R) (x : Rbar) :
  is_lim (fun _ ⇒ a) x a.
Lemma ex_lim_const (a : R) (x : Rbar) :
  ex_lim (fun _ ⇒ a) x.
Lemma Lim_const (a : R) (x : Rbar) :
  Lim (fun _ ⇒ a) x = a.

Lemma is_lim_opp (f : R → R) (x l : Rbar) :
  is_lim f x l → is_lim (fun y ⇒ - f y) x (Rbar_opp l).
Lemma ex_lim_opp (f : R → R) (x : Rbar) :
  ex_lim f x → ex_lim (fun y ⇒ - f y) x.
Lemma Lim_opp (f : R → R) (x : Rbar) :
  Lim (fun y ⇒ - f y) x = Rbar_opp (Lim f x).

Lemma is_lim_plus (f g : R → R) (x lf lg l : Rbar) :
  is_lim f x lf → is_lim g x lg →
  is_Rbar_plus lf lg l →
  is_lim (fun y ⇒ f y + g y) x l.
Lemma is_lim_plus' (f g : R → R) (x : Rbar) (lf lg : R) :
  is_lim f x lf → is_lim g x lg →
  is_lim (fun y ⇒ f y + g y) x (lf + lg).
Lemma ex_lim_plus (f g : R → R) (x : Rbar) :
  ex_lim f x → ex_lim g x →
  ex_Rbar_plus (Lim f x) (Lim g x) →
  ex_lim (fun y ⇒ f y + g y) x.
Lemma Lim_plus (f g : R → R) (x : Rbar) :
  ex_lim f x → ex_lim g x →
  ex_Rbar_plus (Lim f x) (Lim g x) →
  Lim (fun y ⇒ f y + g y) x = Rbar_plus (Lim f x) (Lim g x).

Lemma is_lim_minus (f g : R → R) (x lf lg l : Rbar) :
  is_lim f x lf → is_lim g x lg →
  is_Rbar_minus lf lg l →
  is_lim (fun y ⇒ f y - g y) x l.
Lemma is_lim_minus' (f g : R → R) (x : Rbar) (lf lg : R) :
  is_lim f x lf → is_lim g x lg →
  is_lim (fun y ⇒ f y - g y) x (lf - lg).
Lemma ex_lim_minus (f g : R → R) (x : Rbar) :
  ex_lim f x → ex_lim g x →
  ex_Rbar_minus (Lim f x) (Lim g x) →
  ex_lim (fun y ⇒ f y - g y) x.
Lemma Lim_minus (f g : R → R) (x : Rbar) :
  ex_lim f x → ex_lim g x →
  ex_Rbar_minus (Lim f x) (Lim g x) →
  Lim (fun y ⇒ f y - g y) x = Rbar_minus (Lim f x) (Lim g x).

Lemma is_lim_inv (f : R → R) (x l : Rbar) :
  is_lim f x l → l ≠ 0 → is_lim (fun y ⇒ / f y) x (Rbar_inv l).
Lemma ex_lim_inv (f : R → R) (x : Rbar) :
  ex_lim f x → Lim f x ≠ 0 → ex_lim (fun y ⇒ / f y) x.
Lemma Lim_inv (f : R → R) (x : Rbar) :
  ex_lim f x → Lim f x ≠ 0 → Lim (fun y ⇒ / f y) x = Rbar_inv (Lim f x).

Lemma is_lim_mult (f g : R → R) (x lf lg : Rbar) :
  is_lim f x lf → is_lim g x lg →
  ex_Rbar_mult lf lg →
  is_lim (fun y ⇒ f y × g y) x (Rbar_mult lf lg).
Lemma ex_lim_mult (f g : R → R) (x : Rbar) :
  ex_lim f x → ex_lim g x →
  ex_Rbar_mult (Lim f x) (Lim g x) →
  ex_lim (fun y ⇒ f y × g y) x.
Lemma Lim_mult (f g : R → R) (x : Rbar) :
  ex_lim f x → ex_lim g x →
  ex_Rbar_mult (Lim f x) (Lim g x) →
  Lim (fun y ⇒ f y × g y) x = Rbar_mult (Lim f x) (Lim g x).

Lemma is_lim_scal_l (f : R → R) (a : R) (x l : Rbar) :
  is_lim f x l → is_lim (fun y ⇒ a × f y) x (Rbar_mult a l).
Lemma ex_lim_scal_l (f : R → R) (a : R) (x : Rbar) :
  ex_lim f x → ex_lim (fun y ⇒ a × f y) x.
Lemma Lim_scal_l (f : R → R) (a : R) (x : Rbar) :
  Lim (fun y ⇒ a × f y) x = Rbar_mult a (Lim f x).

Lemma is_lim_scal_r (f : R → R) (a : R) (x l : Rbar) :
  is_lim f x l → is_lim (fun y ⇒ f y × a) x (Rbar_mult l a).
Lemma ex_lim_scal_r (f : R → R) (a : R) (x : Rbar) :
  ex_lim f x → ex_lim (fun y ⇒ f y × a) x.
Lemma Lim_scal_r (f : R → R) (a : R) (x : Rbar) :
  Lim (fun y ⇒ f y × a) x = Rbar_mult (Lim f x) a.

Lemma is_lim_div (f g : R → R) (x lf lg : Rbar) :
  is_lim f x lf → is_lim g x lg → lg ≠ 0 →
  ex_Rbar_div lf lg →
  is_lim (fun y ⇒ f y / g y) x (Rbar_div lf lg).
Lemma ex_lim_div (f g : R → R) (x : Rbar) :
  ex_lim f x → ex_lim g x → Lim g x ≠ 0 →
  ex_Rbar_div (Lim f x) (Lim g x) →
  ex_lim (fun y ⇒ f y / g y) x.
Lemma Lim_div (f g : R → R) (x : Rbar) :
  ex_lim f x → ex_lim g x → Lim g x ≠ 0 →
  ex_Rbar_div (Lim f x) (Lim g x) →
  Lim (fun y ⇒ f y / g y) x = Rbar_div (Lim f x) (Lim g x).

Lemma is_lim_comp_lin (f : R → R) (a b : R) (x l : Rbar) :
  is_lim f (Rbar_plus (Rbar_mult a x) b) l → a ≠ 0
  → is_lim (fun y ⇒ f (a × y + b)) x l.
Lemma ex_lim_comp_lin (f : R → R) (a b : R) (x : Rbar) :
  ex_lim f (Rbar_plus (Rbar_mult a x) b)
  → ex_lim (fun y ⇒ f (a × y + b)) x.
Lemma Lim_comp_lin (f : R → R) (a b : R) (x : Rbar) :
  ex_lim f (Rbar_plus (Rbar_mult a x) b) → a ≠ 0 →
  Lim (fun y ⇒ f (a × y + b)) x = Lim f (Rbar_plus (Rbar_mult a x) b).

Lemma is_lim_continuity (f : R → R) (x : R) :
  continuity_pt f x → is_lim f x (f x).
Lemma ex_lim_continuity (f : R → R) (x : R) :
  continuity_pt f x → ex_finite_lim f x.
Lemma Lim_continuity (f : R → R) (x : R) :
  continuity_pt f x → Lim f x = f x.

Lemma C0_extension_right {T : UniformSpace} (f : R → T) lb (a b : R) :
   a < b →
   (∀ c : R, a < c < b → filterlim f (locally c) (locally (f c))) →
   (filterlim f (at_left b) (locally lb)) →
   {g : R → T | (∀ c, a < c → filterlim g (locally c) (locally (g c)))
     ∧ (∀ c : R, c < b → g c = f c) ∧ g b = lb}.
Lemma filterlim_Ropp_left (x : R) :
  filterlim Ropp (at_left x) (at_right (- x)).
Lemma filterlim_Ropp_right (x : R) :
  filterlim Ropp (at_right x) (at_left (- x)).

Lemma C0_extension_left {T : UniformSpace} (f : R → T) la (a b : R) :
   a < b →
   (∀ c : R, a < c < b → filterlim f (locally c) (locally (f c))) →
   (filterlim f (at_right a) (locally la)) →
   {g : R → T | (∀ c, c < b → filterlim g (locally c) (locally (g c)))
     ∧ (∀ c : R, a < c → g c = f c) ∧ g a = la}.

Lemma C0_extension_lt {T : UniformSpace} (f : R → T) la lb (a b : R) :
  a < b →
   (∀ c : R, a < c < b → filterlim f (locally c) (locally (f c))) →
   (filterlim f (at_right a) (locally la)) →
   (filterlim f (at_left b) (locally lb)) →
   {g : R → T | (∀ c, filterlim g (locally c) (locally (g c)))
     ∧ (∀ c : R, a < c < b → g c = f c) ∧ g a = la ∧ g b = lb}.

Lemma C0_extension_le {T : UniformSpace} (f : R → T) (a b : R) :
   (∀ c : R, a ≤ c ≤ b → filterlim f (locally c) (locally (f c))) →
   {g : R → T | (∀ c, filterlim g (locally c) (locally (g c)))
     ∧ (∀ c : R, a ≤ c ≤ b → g c = f c)}.

Lemma bounded_continuity {K : AbsRing} {V : NormedModule K}
  (f : R → V) a b :
  (∀ x, a ≤ x ≤ b → filterlim f (locally x) (locally (f x)))
  → {M : R | ∀ x, a ≤ x ≤ b → norm (f x) < M}.

Lemma is_lim_le_loc (f g : R → R) (x lf lg : Rbar) :
  Rbar_locally' x (fun y ⇒ f y ≤ g y) →
  is_lim f x lf → is_lim g x lg →
  Rbar_le lf lg.

Lemma is_lim_le_p_loc (f g : R → R) (x : Rbar) :
  Rbar_locally' x (fun y ⇒ f y ≤ g y) →
  is_lim f x p_infty →
  is_lim g x p_infty.

Lemma is_lim_le_m_loc (f g : R → R) (x : Rbar) :
  Rbar_locally' x (fun y ⇒ g y ≤ f y) →
  is_lim f x m_infty →
  is_lim g x m_infty.

Lemma is_lim_le_le_loc (f g h : R → R) (x : Rbar) (l : Rbar) :
  Rbar_locally' x (fun y ⇒ f y ≤ h y ≤ g y) →
  is_lim f x l → is_lim g x l →
  is_lim h x l.

Lemma IVT_gen (f : R → R) (a b y : R) :
  Ranalysis1.continuity f
  → Rmin (f a) (f b) ≤ y ≤ Rmax (f a) (f b)
  → { x : R | Rmin a b ≤ x ≤ Rmax a b ∧ f x = y }.

Lemma IVT_Rbar_incr (f : R → R) (a b la lb : Rbar) (y : R) :
  is_lim f a la → is_lim f b lb
  → (∀ (x : R), Rbar_lt a x → Rbar_lt x b → continuity_pt f x)
  → Rbar_lt a b
  → Rbar_lt la y ∧ Rbar_lt y lb
  → {x : R | Rbar_lt a x ∧ Rbar_lt x b ∧ f x = y}.

Lemma IVT_Rbar_decr (f : R → R) (a b la lb : Rbar) (y : R) :
  is_lim f a la → is_lim f b lb
  → (∀ (x : R), Rbar_lt a x → Rbar_lt x b → continuity_pt f x)
  → Rbar_lt a b
  → Rbar_lt lb y ∧ Rbar_lt y la
  → {x : R | Rbar_lt a x ∧ Rbar_lt x b ∧ f x = y}.

Definition continuity_2d_pt f x y :=
  ∀ eps : posreal, locally_2d (fun u v ⇒ Rabs (f u v - f x y) < eps) x y.

Lemma continuity_2d_pt_filterlim :
  ∀ f x y,
  continuity_2d_pt f x y ↔
  filterlim (fun z : R × R ⇒ f (fst z) (snd z)) (locally (x,y)) (locally (f x y)).

Lemma uniform_continuity_2d :
  ∀ f a b c d,
  (∀ x y, a ≤ x ≤ b → c ≤ y ≤ d → continuity_2d_pt f x y) →
  ∀ eps : posreal, ∃ delta : posreal,
  ∀ x y u v,
  a ≤ x ≤ b → c ≤ y ≤ d →
  a ≤ u ≤ b → c ≤ v ≤ d →
  Rabs (u - x) < delta → Rabs (v - y) < delta →
  Rabs (f u v - f x y) < eps.

Lemma uniform_continuity_2d_1d :
  ∀ f a b c,
  (∀ x, a ≤ x ≤ b → continuity_2d_pt f x c) →
  ∀ eps : posreal, ∃ delta : posreal,
  ∀ x y u v,
  a ≤ x ≤ b → c - delta ≤ y ≤ c + delta →
  a ≤ u ≤ b → c - delta ≤ v ≤ c + delta →
  Rabs (u - x) < delta →
  Rabs (f u v - f x y) < eps.

Lemma uniform_continuity_2d_1d' :
  ∀ f a b c,
  (∀ x, a ≤ x ≤ b → continuity_2d_pt f c x) →
  ∀ eps : posreal, ∃ delta : posreal,
  ∀ x y u v,
  a ≤ x ≤ b → c - delta ≤ y ≤ c + delta →
  a ≤ u ≤ b → c - delta ≤ v ≤ c + delta →
  Rabs (u - x) < delta →
  Rabs (f v u - f y x) < eps.

Lemma continuity_2d_pt_neq_0 :
  ∀ f x y,
  continuity_2d_pt f x y → f x y ≠ 0 →
  locally_2d (fun u v ⇒ f u v ≠ 0) x y.

Lemma continuity_pt_id :
  ∀ x, continuity_pt (fun x ⇒ x) x.

Lemma continuity_2d_pt_id1 :
  ∀ x y, continuity_2d_pt (fun u v ⇒ u) x y.

Lemma continuity_2d_pt_id2 :
  ∀ x y, continuity_2d_pt (fun u v ⇒ v) x y.

Lemma continuity_2d_pt_const :
  ∀ x y c, continuity_2d_pt (fun u v ⇒ c) x y.

Lemma continuity_pt_ext_loc :
  ∀ f g x,
  locally x (fun x ⇒ f x = g x) →
  continuity_pt f x → continuity_pt g x.

Lemma continuity_pt_ext :
  ∀ f g x,
  (∀ x, f x = g x) →
  continuity_pt f x → continuity_pt g x.

Lemma continuity_2d_pt_ext_loc :
  ∀ f g x y,
  locally_2d (fun u v ⇒ f u v = g u v) x y →
  continuity_2d_pt f x y → continuity_2d_pt g x y.

Lemma continuity_2d_pt_ext :
  ∀ f g x y,
  (∀ x y, f x y = g x y) →
  continuity_2d_pt f x y → continuity_2d_pt g x y.

Lemma continuity_1d_2d_pt_comp :
  ∀ f g x y,
  continuity_pt f (g x y) →
  continuity_2d_pt g x y →
  continuity_2d_pt (fun x y ⇒ f (g x y)) x y.

Lemma continuity_2d_pt_opp (f : R → R → R) (x y : R) :
  continuity_2d_pt f x y →
  continuity_2d_pt (fun u v ⇒ - f u v) x y.

Lemma continuity_2d_pt_plus (f g : R → R → R) (x y : R) :
  continuity_2d_pt f x y →
  continuity_2d_pt g x y →
  continuity_2d_pt (fun u v ⇒ f u v + g u v) x y.

Lemma continuity_2d_pt_minus (f g : R → R → R) (x y : R) :
  continuity_2d_pt f x y →
  continuity_2d_pt g x y →
  continuity_2d_pt (fun u v ⇒ f u v - g u v) x y.

Lemma continuity_2d_pt_inv (f : R → R → R) (x y : R) :
  continuity_2d_pt f x y →
  f x y ≠ 0 →
  continuity_2d_pt (fun u v ⇒ / f u v) x y.

Lemma continuity_2d_pt_mult (f g : R → R → R) (x y : R) :
  continuity_2d_pt f x y →
  continuity_2d_pt g x y →
  continuity_2d_pt (fun u v ⇒ f u v × g u v) x y.

Section Continuity.

Context {T U : UniformSpace}.

Definition continuous_on (D : T → Prop) (f : T → U) :=
  ∀ x, D x → filterlim f (within D (locally x)) (locally (f x)).

Definition continuous (f : T → U) (x : T) :=
  filterlim f (locally x) (locally (f x)).

Lemma continuous_continuous_on :
  ∀ (D : T → Prop) (f : T → U) (x : T),
  locally x D →
  continuous_on D f →
  continuous f x.

Lemma continuous_on_subset :
  ∀ (D E : T → Prop) (f : T → U),
  (∀ x, E x → D x) →
  continuous_on D f →
  continuous_on E f.

Lemma continuous_on_forall :
  ∀ (D : T → Prop) (f : T → U),
  (∀ x, D x → continuous f x) →
  continuous_on D f.

Lemma continuous_ext_loc (f g : T → U) (x : T) :
  locally x (fun y : T ⇒ g y = f y)
  → continuous g x → continuous f x.
Lemma continuous_ext :
  ∀ (f g : T → U) (x : T),
  (∀ x, f x = g x) →
  continuous f x →
  continuous g x.

Lemma continuous_on_ext :
  ∀ (D : T → Prop) (f g : T → U),
  (∀ x, D x → f x = g x) →
  continuous_on D f →
  continuous_on D g.

End Continuity.

Lemma continuous_comp {U V W : UniformSpace} (f : U → V) (g : V → W) (x : U) :
  continuous f x → continuous g (f x)
  → continuous (fun x ⇒ g (f x)) x.
Lemma continuous_comp_2 {U V W X : UniformSpace}
  (f : U → V) (g : U → W) (h : V → W → X) (x : U) :
  continuous f x → continuous g x
  → continuous (fun (x : V × W) ⇒ h (fst x) (snd x)) (f x,g x)
  → continuous (fun x ⇒ h (f x) (g x)) x.

Lemma is_lim_comp_continuous (f g : R → R) (x : Rbar) (l : R) :
  is_lim f x l → continuous g l
    → is_lim (fun x ⇒ g (f x)) x (g l).

Lemma continuous_fst {U V : UniformSpace} (x : U) (y : V) :
  continuous (fst (B:=V)) (x, y).
Lemma continuous_snd {U V : UniformSpace} (x : U) (y : V) :
  continuous (snd (B:=V)) (x, y).

Lemma continuous_const {U V : UniformSpace} (c : V) (x : U) :
  continuous (fun _ ⇒ c) x.

Lemma continuous_id {U : UniformSpace} (x : U) :
  continuous (fun y ⇒ y) x.

Section Continuity_op.

Context {U : UniformSpace} {K : AbsRing} {V : NormedModule K}.

Lemma continuous_opp (f : U → V) (x : U) :
  continuous f x →
  continuous (fun x : U ⇒ opp (f x)) x.

Lemma continuous_plus (f g : U → V) (x : U) :
  continuous f x → continuous g x →
  continuous (fun x : U ⇒ plus (f x) (g x)) x.

Lemma continuous_minus (f g : U → V) (x : U) :
  continuous f x → continuous g x →
  continuous (fun x : U ⇒ minus (f x) (g x)) x.

Lemma continuous_scal (k : U → K) (f : U → V) (x : U) :
  continuous k x → continuous f x → continuous (fun y ⇒ scal (k y) (f y)) x.
Lemma continuous_scal_r (k : K) (f : U → V) (x : U) :
  continuous f x → continuous (fun y ⇒ scal k (f y)) x.
Lemma continuous_scal_l (f : U → K) (k : V) (x : U) :
  continuous f x → continuous (fun y ⇒ scal (f y) k) x.

End Continuity_op.

Lemma continuous_mult {U : UniformSpace} {K : AbsRing}
  (f g : U → K) (x : U) :
  continuous f x → continuous g x
  → continuous (fun y ⇒ mult (f y) (g y)) x.

Section UnifCont.

Context {V : UniformSpace}.

Lemma unifcont_1d (f : R → V) a b :
  (∀ x, a ≤ x ≤ b → continuous f x) →
  ∀ eps : posreal, {delta : posreal | ∀ x y,
    a ≤ x ≤ b → a ≤ y ≤ b → ball x delta y → ~~ ball (f x) eps (f y)}.

End UnifCont.

Section UnifCont_N.

Context {K : AbsRing} {V : NormedModule K}.

Lemma unifcont_normed_1d (f : R → V) a b :
  (∀ x, a ≤ x ≤ b → continuous f x) →
  ∀ eps : posreal, {delta : posreal | ∀ x y,
    a ≤ x ≤ b → a ≤ y ≤ b → ball x delta y → ball_norm (f x) eps (f y)}.

End UnifCont_N.