From 4f9adc1845a949f8ace5a196f911c9ccdf3ce52b Mon Sep 17 00:00:00 2001 From: Aaron Liu Date: Tue, 19 May 2026 18:32:48 -0400 Subject: [PATCH 1/4] free --- Mathlib/Topology/Compactness/CountablyCompact.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Mathlib/Topology/Compactness/CountablyCompact.lean b/Mathlib/Topology/Compactness/CountablyCompact.lean index df37e4a99cfc55..c9b35dda233e8f 100644 --- a/Mathlib/Topology/Compactness/CountablyCompact.lean +++ b/Mathlib/Topology/Compactness/CountablyCompact.lean @@ -261,9 +261,9 @@ instance (priority := 50) [SequentialSpace E] [CountablyCompactSpace E] : · simp only [image_eq_iUnion, mem_Ici, iUnion_ge_eq_iUnion_nat_add _ (k + 1)] exact iUnion_mono fun i => subset_closure -/-- If `f : X → Y` is an embedding map, the image `f '' s` of a set `s` is sequentially compact +/-- If `f : X → Y` is an inducing map, the image `f '' s` of a set `s` is sequentially compact if and only if `s` is sequentially compact. -/ -theorem Topology.IsEmbedding.isSeqCompact_iff {f : E → F} (hf : IsEmbedding f) : +theorem Topology.IsInducing.isSeqCompact_iff {f : E → F} (hf : IsInducing f) : IsSeqCompact A ↔ IsSeqCompact (f '' A) where mp hA x hx := by choose y hy using hx @@ -358,7 +358,7 @@ theorem IsLindelof.isCompact (hA : IsCountablyCompact A) (hl : IsLindelof A) : · exact ⟨∅, by simp_all⟩ /-- A countably compact Lindelöf space is compact. -/ -theorem LindelofSpace.CompactSpace {X : Type*} [TopologicalSpace X] +theorem LindelofSpace.compactSpace {X : Type*} [TopologicalSpace X] [LindelofSpace X] [h : CountablyCompactSpace X] : CompactSpace X where isCompact_univ := isLindelof_univ.isCompact h.isCountablyCompact_univ From e3e7ca087895f659f567fdee6280f273cb60af7a Mon Sep 17 00:00:00 2001 From: Aaron Liu Date: Tue, 19 May 2026 19:45:46 -0400 Subject: [PATCH 2/4] add deprecation --- Mathlib/Topology/Compactness/CountablyCompact.lean | 3 +++ 1 file changed, 3 insertions(+) diff --git a/Mathlib/Topology/Compactness/CountablyCompact.lean b/Mathlib/Topology/Compactness/CountablyCompact.lean index c9b35dda233e8f..2d6527a0ab3aee 100644 --- a/Mathlib/Topology/Compactness/CountablyCompact.lean +++ b/Mathlib/Topology/Compactness/CountablyCompact.lean @@ -362,6 +362,9 @@ theorem LindelofSpace.compactSpace {X : Type*} [TopologicalSpace X] [LindelofSpace X] [h : CountablyCompactSpace X] : CompactSpace X where isCompact_univ := isLindelof_univ.isCompact h.isCountablyCompact_univ +@[deprecated (since := "2026-05-19")] +alias LindelofSpace.CompactSpace := LindelofSpace.compactSpace + /-- In a Hereditarily Lindelöf space, a countably compact set is compact. -/ theorem IsCountablyCompact.isCompact [HereditarilyLindelofSpace E] (hA : IsCountablyCompact A) : IsCompact A := From f8c701eefe04c95b14ebc3242a4665b82eb12d3a Mon Sep 17 00:00:00 2001 From: Aaron Liu Date: Sat, 23 May 2026 18:02:05 -0400 Subject: [PATCH 3/4] add deprecation :((( --- Mathlib/Topology/Compactness/CountablyCompact.lean | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/Mathlib/Topology/Compactness/CountablyCompact.lean b/Mathlib/Topology/Compactness/CountablyCompact.lean index 2d6527a0ab3aee..06181b9b92e84f 100644 --- a/Mathlib/Topology/Compactness/CountablyCompact.lean +++ b/Mathlib/Topology/Compactness/CountablyCompact.lean @@ -276,9 +276,12 @@ theorem Topology.IsInducing.isSeqCompact_iff {f : E → F} (hf : IsInducing f) : choose a ha using hfa exact ⟨a, ha.1, φ, hφ.1, hf.tendsto_nhds_iff.2 (ha.2 ▸ hφ.2)⟩ +@[deprecated (since := "2026-05-23")] +alias Topology.IsEmbedding.isSeqCompact_iff := Topology.IsInducing.isSeqCompact_iff + theorem Subtype.isSeqCompact_iff {p : E → Prop} {A : Set { x // p x }} : IsSeqCompact A ↔ IsSeqCompact ((↑) '' A : Set E) := - IsEmbedding.subtypeVal.isSeqCompact_iff + IsEmbedding.subtypeVal.toIsInducing.isSeqCompact_iff theorem isSeqCompact_iff_isSeqCompact_univ : IsSeqCompact A ↔ IsSeqCompact (univ : Set A) := by rw [Subtype.isSeqCompact_iff, image_univ, Subtype.range_coe] From c640c96d5f217450452c7d181aa133a17e23b03d Mon Sep 17 00:00:00 2001 From: Aaron Liu Date: Tue, 2 Jun 2026 22:51:47 -0400 Subject: [PATCH 4/4] unadd deprecation :) This reverts commit f8c701eefe04c95b14ebc3242a4665b82eb12d3a. --- Mathlib/Topology/Compactness/CountablyCompact.lean | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/Mathlib/Topology/Compactness/CountablyCompact.lean b/Mathlib/Topology/Compactness/CountablyCompact.lean index 06181b9b92e84f..2d6527a0ab3aee 100644 --- a/Mathlib/Topology/Compactness/CountablyCompact.lean +++ b/Mathlib/Topology/Compactness/CountablyCompact.lean @@ -276,12 +276,9 @@ theorem Topology.IsInducing.isSeqCompact_iff {f : E → F} (hf : IsInducing f) : choose a ha using hfa exact ⟨a, ha.1, φ, hφ.1, hf.tendsto_nhds_iff.2 (ha.2 ▸ hφ.2)⟩ -@[deprecated (since := "2026-05-23")] -alias Topology.IsEmbedding.isSeqCompact_iff := Topology.IsInducing.isSeqCompact_iff - theorem Subtype.isSeqCompact_iff {p : E → Prop} {A : Set { x // p x }} : IsSeqCompact A ↔ IsSeqCompact ((↑) '' A : Set E) := - IsEmbedding.subtypeVal.toIsInducing.isSeqCompact_iff + IsEmbedding.subtypeVal.isSeqCompact_iff theorem isSeqCompact_iff_isSeqCompact_univ : IsSeqCompact A ↔ IsSeqCompact (univ : Set A) := by rw [Subtype.isSeqCompact_iff, image_univ, Subtype.range_coe]