Commit 2026-01-15 23:42 3734333e

feat(Topology): generalize tendsto_inv_iff from ℝ≥0∞ to ContinuousInv + InvolutiveInv (#33920) 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.