[Merged by Bors] - feat(Topology): generalize tendsto_inv_iff from ℝ≥0∞ to ContinuousInv + InvolutiveInv

[Citronhat]

This PR implements the TODO in Topology.Instances.ENNReal.Lemmas by moving the lemma to a more general setting.

• Add a general lemma tendsto_inv_iff in Topology.Algebra.Group.Basic (with @[simp]), whose proof is the same as the previous ℝ≥0∞ proof, just stated for an arbitrary G with [InvolutiveInv G] and [ContinuousInv G].

• Mark it @[to_additive (attr := simp)], so the additive analogue is generated automatically.

• Deprecate ENNReal.tendsto_inv_iff in Topology.Instances.ENNReal.Lemmas.

No mathematical content changes: this is a relocation/deprecation of the existing theorem plus the additive version.

[github-actions]

PR summary 3de2350c1f

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+-+ tendsto_inv_iff

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).

[vihdzp]

Otherwise LGTM

[ADedecker]

I took the liberty of making the title of your PR more precise: the first one sounded a bit weird given that ℝ≥0∞ is not a topological group... Do not hesitate to change to something else if you prefer.

bors d+

[mathlib-bors]

✌️ Citronhat can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[Citronhat]

I took the liberty of making the title of your PR more precise: the first one sounded a bit weird given that ℝ≥0∞ is not a topological group... Do not hesitate to change to something else if you prefer.

Fair enough. I was close to changing it myself, but I ended up convinced myself that the more readable title justified the "lie".

By the way, I have a couple of related questions regarding design philosophy that I hope one of you can clarify:

• Specialization Policy: When do we provide specialized versions of general ones? I am looking at some of the TODOs in Data.ENNReal.Operations, where many of the theorems have one-line proofs from WithTop. Why do we want such theorems there, but not an ENNReal.tendsto_inv_iff?

• Scope of Generalization: I am also considering generalizing a few other ENNReal results to WithTop that are not tagged with a TODO. I guess it would be meaningless to generalize ENNReal theorems to WithTop if the assumptions needed are so strong that ENNReal is the only practical instance. And if an ENNReal theorem is already a simple one-line proof, there is also not much to be gained. But otherwise, why not prove them as WithTop?

I would appreciate any insights you have time to share :)

[Citronhat]

bors r+

[mathlib-bors]

Build failed:

• Post-Build Step

[Citronhat]

bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style
• Post-Build Step