feat: Fin.init and Fin.tail are continuous

[scholzhannah]

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.

---

[github-actions]

PR summary d40c80aac1

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ Continuous.finInit
+ Continuous.finTail
+ ContinuousAt.finInit
+ ContinuousAt.finTail
+ Filter.Tendsto.finInit
+ Filter.Tendsto.finTail

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[eric-wieser]

Thanks, this now looks good. I found some alternative proofs using Pi.precomp_continuous, but they're not really any shorter than these.

Could you add a sentence in the PR description explaining what you were doing when you needed these?

[scholzhannah]

Could you add a sentence in the PR description explaining what you were doing when you needed these?

Sure!