Linear map is continuous if it's continuous at zero

Stream: Is there code for X?

[Bhavik Mehta]

Here's my goal:

import data.real.basic
import topology.algebra.ordered
import topology.instances.real
import analysis.normed_space.operator_norm

noncomputable theory

lemma continuous_linear_map_of_continuous_at_zero {E F : Type*} [normed_group E] [normed_space ℝ E]
  [normed_group F] [normed_space ℝ F] (f : E →ₗ[ℝ] F) (hf : continuous_at f (0:E)):
  continuous f :=
begin

end

The closest things I can see in mathlib are to strengthen docs#multilinear_map.exists_bound_of_continuous (its proof only actually uses continuity at zero anyway) and then use docs#linear_map.continuous_of_bound but is there a more direct way?

[Patrick Massot]

open filter
open_locale topological_space

lemma continuous_linear_map_of_continuous_at_zero {E F : Type*} [normed_group E] [normed_space ℝ E]
  [normed_group F] [normed_space ℝ F] (f : E →ₗ[ℝ] F) (hf : continuous_at f (0:E)):
  continuous f :=
begin
  have : tendsto f (𝓝 0) (𝓝 0), by simpa using hf.tendsto,
  exact (uniform_continuous_of_tendsto_zero this).continuous,
end

[Bhavik Mehta]

Amazing, thank you Patrick!

[Bhavik Mehta]

Here was the attempt I'd just finished up, yours is much nicer :)

lemma continuous_linear_map_of_continuous_at_zero {E F : Type*} [normed_group E] [normed_space ℝ E]
  [normed_group F] [normed_space ℝ F] (f : E →ₗ[ℝ] F) (hf : continuous_at f (0:E)):
  continuous f :=
begin
  rw continuous_iff_continuous_at,
  intros x,
  change filter.tendsto _ _ _,
  change filter.tendsto _ _ _ at hf,
  rw normed_group.tendsto_nhds_nhds at ⊢ hf,
  intros ε hε,
  obtain ⟨δ, hδ₁, hδ₂⟩ := hf ε hε,
  refine ⟨δ, hδ₁, λ x' hx', by simpa using hδ₂ (x' - x) (by simpa using hx')⟩,
end

[Patrick Massot]

I don't know why this isn't in mathlib.

[Patrick Massot]

maybe it is somewhere

[Patrick Massot]

Regarding your proof: the main hint is this lemma has nothing to do with norms.

[Patrick Massot]

lemma continuous_group_hom_of_continuous_at_zero {E F : Type*}
  [add_comm_group E] [add_comm_group F] [uniform_space E] [uniform_add_group E]
  [uniform_space F] [uniform_add_group F]  (f : E →+ F) (hf : continuous_at f (0:E)) :
  continuous f :=
begin
  have : tendsto f (𝓝 0) (𝓝 0), by simpa using hf.tendsto,
  exact (uniform_continuous_of_tendsto_zero this).continuous,
end

[Patrick Massot]

(also nothing to do with scalar multiplication)