feat: Fin.init and Fin.tail are continuous (#22550)

I needed the continuity of `Fin.init` for the inductive CW structure on the sphere. There the inverses of the characteristic maps are just the projections of the upper and lower hemisphere onto the obvious hyperplane. It was easiest to use `Fin.init` for this.

Author: scholzhannah

Mathlib/Topology/Constructions.lean

@@ -824,6 +824,34 @@ theorem Continuous.finInsertNth
 @[deprecated (since := "2025-01-02")]
 alias Continuous.fin_insertNth := Continuous.finInsertNth
 
+theorem Filter.Tendsto.finInit {f : Y → ∀ j : Fin (n + 1), π j} {l : Filter Y} {x : ∀ j, π j}
+    (hg : Tendsto f l (𝓝 x)) : Tendsto (fun a ↦ Fin.init (f a)) l (𝓝 <| Fin.init x) :=
+  tendsto_pi_nhds.2 fun j ↦ apply_nhds hg j.castSucc
+
+@[fun_prop]
+theorem ContinuousAt.finInit {f : X → ∀ j : Fin (n + 1), π j} {x : X}
+    (hf : ContinuousAt f x) : ContinuousAt (fun a ↦ Fin.init (f a)) x :=
+  hf.tendsto.finInit
+
+@[fun_prop]
+theorem Continuous.finInit {f : X → ∀ j : Fin (n + 1), π j} (hf : Continuous f) :
+    Continuous fun a ↦ Fin.init (f a) :=
+  continuous_iff_continuousAt.2 fun _ ↦ hf.continuousAt.finInit
+
+theorem Filter.Tendsto.finTail {f : Y → ∀ j : Fin (n + 1), π j} {l : Filter Y} {x : ∀ j, π j}
+    (hg : Tendsto f l (𝓝 x)) : Tendsto (fun a ↦ Fin.tail (f a)) l (𝓝 <| Fin.tail x) :=
+  tendsto_pi_nhds.2 fun j ↦ apply_nhds hg j.succ
+
+@[fun_prop]
+theorem ContinuousAt.finTail {f : X → ∀ j : Fin (n + 1), π j} {x : X}
+    (hf : ContinuousAt f x) : ContinuousAt (fun a ↦ Fin.tail (f a)) x :=
+  hf.tendsto.finTail
+
+@[fun_prop]
+theorem Continuous.finTail {f : X → ∀ j : Fin (n + 1), π j} (hf : Continuous f) :
+    Continuous fun a ↦ Fin.tail (f a) :=
+  continuous_iff_continuousAt.2 fun _ ↦ hf.continuousAt.finTail
+
 end Fin
 
 theorem isOpen_set_pi {i : Set ι} {s : ∀ a, Set (π a)} (hi : i.Finite)