[Merged by Bors] - chore(Topology/Compactness/CountablyCompact): generalize theorem

[plp127]

Generalize theorem Topology.IsEmbedding.isSeqCompact_iff to Topology.IsInducing.isSeqCompact_iff by replacing IsEmbedding by IsInducing.

Also fix capitalization error.

---

[github-actions]

PR summary 7b9b73e717

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ LindelofSpace.compactSpace
+ Topology.IsInducing.isSeqCompact_iff
- Topology.IsEmbedding.isSeqCompact_iff

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

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

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit 7b9b73e717
Reference commit 45edb79497

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/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).

[grunweg]

Thanks! This looks straightforward, except for the deprecation question. (I think either way is probably fine.)
If a second maintainer feels strongly, I'll let them comment within the next 24h (and otherwise merge myself).
maintainer merge?

[j-loreaux]

@plp127 I think the material is new enough and the chance be being bitten by this particular deprecation rare enough, that it doesn't matter whether or not we add the deprecation (for IsInducing). I'll leave it up to you.

bors d+

[mathlib-bors]

✌️ plp127 can now approve this pull request until 2026-06-17 02:44 UTC (in 2 weeks). To approve and merge, reply with bors r+. More detailed instructions are available here.

[plp127]

bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• ci (staging) / Lint style
• ci (staging) / Post-CI job
• ci (staging) / Build
• ci (staging) / Post-Build Step