## Stream: Is there code for X?

### Topic: Linear map is continuous if it's continuous at zero

#### Bhavik Mehta (Apr 15 2021 at 16:49):

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 (Apr 15 2021 at 16:56):

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 (Apr 15 2021 at 16:56):

Amazing, thank you Patrick!

#### Bhavik Mehta (Apr 15 2021 at 16:56):

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 (Apr 15 2021 at 16:56):

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

#### Patrick Massot (Apr 15 2021 at 16:57):

maybe it is somewhere

#### Patrick Massot (Apr 15 2021 at 16:59):

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

#### Patrick Massot (Apr 15 2021 at 16:59):

lemma continuous_group_hom_of_continuous_at_zero {E F : Type*}
[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 (Apr 15 2021 at 16:59):

(also nothing to do with scalar multiplication)

Last updated: May 19 2021 at 03:22 UTC