Continuity means left limit equals right limit

Stream: new members

[Tony Ma]

How to decompose continuity into left and right limit? I am not familiar with filter language, so I don't know how to search for the answer.

example {f : ℝ → ℝ} (hf : ∀ x, x ≤ 0 → f x = x) (hf' : ∀ x, x > 0 → f x = x ^ 2) :
    Continuous f := by

[Luigi Massacci]

see docs#continuousAt_iff_continuous_left_right

[Tony Ma]

Ok. But in the reverse way, given (hf : ∀ x, x ≤ 0 → f x = x) (hf' : ∀ x, x > 0 → f x = x ^ 2 + a) ($a$ is a real number), how can I show that $a = 0$ by ContinuousWithinAt f (Set.Ici 0) 0 (which I got from continuousAt_iff_continuous_left_right)?

[Luigi Massacci]

I would say you should provide the rest of the context, if you make an #mwe it's easier to help you. (Also the usual first thing to do is think about how you would prove it on paper)

[Luigi Massacci]

Oh btw, did you just try by continuity at the beginning?

[Luigi Massacci]

I doubt it will work, but it's always worth it to try

[Tony Ma]

Ok. What I mean is something like

example {a : ℝ} {f : ℝ → ℝ} (hf : ∀ x, x ≤ 0 → f x = x) (hf' : ∀ x, x > 0 → f x = x + a) (f_cont : Continuous f): a = 0 := by
  sorry

I tried by continuity to prove f 0 = 0 + a but it doesn't seem to be right. Maybe I use it wrongly.
(The proof on paper I suggest is that we have $f(0)=0+a$ by considering hypothesis hf'. But I don't know how to deal with left or right limits, so on.)

[Etienne Marion]

Here is a way:

import Mathlib

open Filter Topology

example {a : ℝ} {f : ℝ → ℝ} (hf : ∀ x, x ≤ 0 → f x = x) (hf' : ∀ x, x > 0 → f x = x + a) (f_cont : Continuous f) : a = 0 := by
  have h1 : Tendsto f (𝓝[≤] 0) (𝓝 (f 0)) := (f_cont.tendsto 0).mono_left nhdsWithin_le_nhds
  have h2 : Tendsto f (𝓝[>] 0) (𝓝 (f 0)) := (f_cont.tendsto 0).mono_left nhdsWithin_le_nhds
  have h3 : Tendsto f (𝓝[≤] 0) (𝓝 0) := by
    apply tendsto_nhdsWithin_congr (f := id)
    simpa using (fun x hx ↦ (hf x hx).symm)
    exact (continuous_id.tendsto 0).mono_left nhdsWithin_le_nhds
  have h4 : Tendsto f (𝓝[>] 0) (𝓝 a) := by
    apply tendsto_nhdsWithin_congr (f := fun x ↦ x + a)
    simpa using (fun x hx ↦ (hf' x hx).symm)
    simpa using ((continuous_add_right a).tendsto 0).mono_left nhdsWithin_le_nhds
  rw [← tendsto_nhds_unique h1 h3, ← tendsto_nhds_unique h2 h4]