Implement proofs for ContinuousWithinAt.tfae and Exercises 9.4.6 & 9.4.7

[younesselassri08-maker]

This PR implements missing proofs for Section 9.4. Specifically, I established the equivalence of continuity definitions in "ContinuousWithinAt.tfae" (Prop 9.4.7) by bridging the topological, sequential, and metric definitions via manual logical rewriting. I implemented the proof for "ContinuousOn.restrict" (Exercise 9.4.7), demonstrating that a function continuous on a set X remains continuous on any subset Y of X. Finally, I completed Exercise 9.4.6 by proving the continuity of polynomial functions "Continuous.polynomial" using induction and the course's sum/product rules.

[teorth]

Thank you, but the intention of the master repository is not to fill in the sorries that are assigned to exercises. You are free to create forks of the master repository with these proofs. You can also add hints or tips to the docstring at the start of the lean files for the exercises (this is only fully implemented for the first few chapters, but feel free to add hints for later chapters as well).