From 36a2015278a65ba6b0f27e06a480b50cb8dd0919 Mon Sep 17 00:00:00 2001
From: Anatole Dedecker <anatolededecker@gmail.com>
Date: Tue, 26 Oct 2021 21:02:25 +0000
Subject: [PATCH] feat(topology/[separation, dense_embedding]): a function to a
 T1 space which has a limit at x is continuous at x (#9934)

We prove that, for a function `f` with values in a T1 space, knowing that `f` admits *any* limit at `x` suffices to prove that `f` is continuous at `x`.

We then use it to give a variant of `dense_inducing.extend_eq` with the same assumption required for continuity of the extension, which makes using both `extend_eq` and `continuous_extend` easier, and also brings us closer to Bourbaki who makes no explicit continuity assumption on the function to extend.
---
 src/topology/algebra/uniform_field.lean       |  2 +-
 src/topology/dense_embedding.lean             | 20 +++++++++++++++++--
 src/topology/separation.lean                  | 15 ++++++++++++++
 .../uniform_space/uniform_embedding.lean      |  2 +-
 4 files changed, 35 insertions(+), 4 deletions(-)

diff --git a/src/topology/algebra/uniform_field.lean b/src/topology/algebra/uniform_field.lean
index 1f7b16963a5a5..2125b4d4e9059 100644
--- a/src/topology/algebra/uniform_field.lean
+++ b/src/topology/algebra/uniform_field.lean
@@ -92,7 +92,7 @@ instance completion.has_inv : has_inv (hat K) := ⟨λ x, if x = 0 then 0 else h
 variables [topological_division_ring K]
 
 lemma hat_inv_extends {x : K} (h : x ≠ 0) : hat_inv (x : hat K) = coe (x⁻¹ : K) :=
-dense_inducing_coe.extend_eq_at _
+dense_inducing_coe.extend_eq_at
     ((continuous_coe K).continuous_at.comp (topological_division_ring.continuous_inv x h))
 
 variables [completable_top_field K]
diff --git a/src/topology/dense_embedding.lean b/src/topology/dense_embedding.lean
index d4dad464ec209..11e823342d91b 100644
--- a/src/topology/dense_embedding.lean
+++ b/src/topology/dense_embedding.lean
@@ -121,13 +121,29 @@ lemma extend_eq_of_tendsto [t2_space γ] {b : β} {c : γ} {f : α → γ}
   di.extend f b = c :=
 by haveI := di.comap_nhds_ne_bot; exact hf.lim_eq
 
-lemma extend_eq_at [t2_space γ] {f : α → γ} (a : α) (hf : continuous_at f a) :
+lemma extend_eq_at [t2_space γ] {f : α → γ} {a : α} (hf : continuous_at f a) :
   di.extend f (i a) = f a :=
 extend_eq_of_tendsto _ $ di.nhds_eq_comap a ▸ hf
 
+lemma extend_eq_at' [t2_space γ] {f : α → γ} {a : α} (c : γ) (hf : tendsto f (𝓝 a) (𝓝 c)) :
+  di.extend f (i a) = f a :=
+di.extend_eq_at (continuous_at_of_tendsto_nhds hf)
+
 lemma extend_eq [t2_space γ] {f : α → γ} (hf : continuous f) (a : α) :
   di.extend f (i a) = f a :=
-di.extend_eq_at a hf.continuous_at
+di.extend_eq_at hf.continuous_at
+
+/-- Variation of `extend_eq` where we ask that `f` has a limit along `comap i (𝓝 b)` for each
+`b : β`. This is a strictly stronger assumption than continuity of `f`, but in a lot of cases
+you'd have to prove it anyway to use `continuous_extend`, so this avoids doing the work twice. -/
+lemma extend_eq' [t2_space γ] {f : α → γ}
+  (di : dense_inducing i) (hf : ∀ b, ∃ c, tendsto f (comap i (𝓝 b)) (𝓝 c)) (a : α) :
+  di.extend f (i a) = f a :=
+begin
+  rcases hf (i a) with ⟨b, hb⟩,
+  refine di.extend_eq_at' b _,
+  rwa ← di.to_inducing.nhds_eq_comap at hb,
+end
 
 lemma extend_unique_at [t2_space γ] {b : β} {f : α → γ} {g : β → γ} (di : dense_inducing i)
   (hf : ∀ᶠ x in comap i (𝓝 b), g (i x) = f x) (hg : continuous_at g b) :
diff --git a/src/topology/separation.lean b/src/topology/separation.lean
index 0b584b05ac7b6..22469d19d4ef8 100644
--- a/src/topology/separation.lean
+++ b/src/topology/separation.lean
@@ -321,6 +321,21 @@ begin
   exact ⟨i, hi, λ h, hsub h rfl⟩
 end
 
+/-- If a function to a `t1_space` tends to some limit `b` at some point `a`, then necessarily
+`b = f a`. -/
+lemma eq_of_tendsto_nhds [topological_space β] [t1_space β] {f : α → β} {a : α} {b : β}
+  (h : tendsto f (𝓝 a) (𝓝 b)) : f a = b :=
+by_contra $ assume (hfa : f a ≠ b),
+have fact₁ : {f a}ᶜ ∈ 𝓝 b := compl_singleton_mem_nhds hfa.symm,
+have fact₂ : tendsto f (pure a) (𝓝 b) := h.comp (tendsto_id' $ pure_le_nhds a),
+fact₂ fact₁ (eq.refl $ f a)
+
+/-- To prove a function to a `t1_space` is continuous at some point `a`, it suffices to prove that
+`f` admits *some* limit at `a`. -/
+lemma continuous_at_of_tendsto_nhds [topological_space β] [t1_space β] {f : α → β} {a : α} {b : β}
+  (h : tendsto f (𝓝 a) (𝓝 b)) : continuous_at f a :=
+show tendsto f (𝓝 a) (𝓝 $ f a), by rwa eq_of_tendsto_nhds h
+
 /-- If the punctured neighborhoods of a point form a nontrivial filter, then any neighborhood is
 infinite. -/
 lemma infinite_of_mem_nhds {α} [topological_space α] [t1_space α] (x : α) [hx : ne_bot (𝓝[{x}ᶜ] x)]
diff --git a/src/topology/uniform_space/uniform_embedding.lean b/src/topology/uniform_space/uniform_embedding.lean
index e3d5d43229cbb..46e2b6aa96a7f 100644
--- a/src/topology/uniform_space/uniform_embedding.lean
+++ b/src/topology/uniform_space/uniform_embedding.lean
@@ -414,7 +414,7 @@ end
 variables [separated_space γ]
 
 lemma uniformly_extend_of_ind (b : β) : ψ (e b) = f b :=
-dense_inducing.extend_eq_at _ b h_f.continuous.continuous_at
+dense_inducing.extend_eq_at _ h_f.continuous.continuous_at
 
 lemma uniformly_extend_unique {g : α → γ} (hg : ∀ b, g (e b) = f b)
   (hc : continuous g) :