Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit 2792979

Browse files
sgouezelsgouezel
committed
chore(topology/*): rename compact_univ to is_compact_univ, and many more (#17436)
Many lemma names about compact sets have `compact` instead of `is_compact` in their names, for historical reasons. We rename several of them to match more closely the naming convention.
1 parent bfad3f4 commit 2792979

47 files changed

Lines changed: 172 additions & 162 deletions

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎docs/overview.yaml‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -233,8 +233,8 @@ Topology:
233233
Metric spaces:
234234
metric space: 'metric_space'
235235
ball: 'metric.ball'
236-
sequential compactness is equivalent to compactness (Bolzano-Weierstrass): 'uniform_space.compact_iff_seq_compact'
237-
Heine-Borel theorem (proper metric space version): 'metric.compact_iff_closed_bounded'
236+
sequential compactness is equivalent to compactness (Bolzano-Weierstrass): 'uniform_space.is_compact_iff_is_seq_compact'
237+
Heine-Borel theorem (proper metric space version): 'metric.is_compact_iff_is_closed_bounded'
238238
Lipschitz continuity: 'lipschitz_with'
239239
Hölder continuity: 'holder_with'
240240
contraction mapping theorem: 'contracting_with.exists_fixed_point'

‎docs/undergrad.yaml‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -289,7 +289,7 @@ Single Variable Real Analysis:
289289
metric structure: 'real.metric_space'
290290
completeness of R: 'real.complete_space'
291291
Bolzano-Weierstrass theorem: 'tendsto_subseq_of_bounded'
292-
compact subsets of $\R$: 'metric.compact_iff_closed_bounded'
292+
compact subsets of $\R$: 'metric.is_compact_iff_is_closed_bounded'
293293
connected subsets of $\R$: 'set_of_is_preconnected_eq_of_ordered'
294294
additive subgroups of $\R$: 'real.subgroup_dense_or_cyclic'
295295
Numerical series:
@@ -400,7 +400,7 @@ Topology:
400400
continuous functions: 'continuous'
401401
homeomorphisms: 'homeomorph'
402402
compactness in terms of open covers (Borel-Lebesgue): 'is_compact_iff_finite_subcover'
403-
sequential compactness is equivalent to compactness (Bolzano-Weierstrass): 'uniform_space.compact_iff_seq_compact'
403+
sequential compactness is equivalent to compactness (Bolzano-Weierstrass): 'uniform_space.is_compact_iff_is_seq_compact'
404404
connectedness: 'connected_space'
405405
connected components: 'connected_component'
406406
path connectedness: 'is_path_connected'

‎roadmap/topology/paracompact.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -55,7 +55,7 @@ lemma paracompact_of_compact {X : Type u} [topological_space X] [compact_space X
5555
begin
5656
refine ⟨λ α u uo uc, _⟩,
5757
obtain ⟨s, _, sf, sc⟩ :=
58-
compact_univ.elim_finite_subcover_image (λ a _, uo a) (by rwa [univ_subset_iff, bUnion_univ]),
58+
is_compact_univ.elim_finite_subcover_image (λ a _, uo a) (by rwa [univ_subset_iff, bUnion_univ]),
5959
refine ⟨s, λ b, u b.val, λ b, uo b.val, _, _, λ b, ⟨b.val, subset.refl _⟩⟩,
6060
{ todo },
6161
{ intro x,

‎src/algebraic_geometry/morphisms/quasi_compact.lean‎

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -94,7 +94,7 @@ begin
9494
intros H U hU hU',
9595
obtain ⟨S, hS, rfl⟩ := (is_compact_open_iff_eq_finset_affine_union U).mp ⟨hU', hU⟩,
9696
simp only [set.preimage_Union, subtype.val_eq_coe],
97-
exact hS.compact_bUnion (λ i _, H i i.prop)
97+
exact hS.is_compact_bUnion (λ i _, H i i.prop)
9898
end
9999

100100
@[simp] lemma quasi_compact.affine_property_to_property {X Y : Scheme} (f : X ⟶ Y) :
@@ -167,7 +167,8 @@ begin
167167
rw ← hS,
168168
dsimp [opens.map],
169169
simp only [opens.coe_supr, set.preimage_Union, subtype.val_eq_coe],
170-
exacts [compact_Union (λ i, is_compact_iff_compact_space.mpr (hS' i)), top_is_affine_open _] }
170+
exacts [is_compact_Union (λ i, is_compact_iff_compact_space.mpr (hS' i)),
171+
top_is_affine_open _] }
171172
end
172173

173174
lemma quasi_compact.affine_open_cover_tfae {X Y : Scheme.{u}} (f : X ⟶ Y) :

‎src/algebraic_geometry/morphisms/quasi_separated.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -243,9 +243,9 @@ begin
243243
obtain ⟨s', hs', e'⟩ := (is_compact_open_iff_eq_basic_open_union _).mp ⟨hV', hV⟩,
244244
rw [e, e', set.Union₂_inter],
245245
simp_rw [set.inter_Union₂],
246-
apply hs.compact_bUnion,
246+
apply hs.is_compact_bUnion,
247247
{ intros i hi,
248-
apply hs'.compact_bUnion,
248+
apply hs'.is_compact_bUnion,
249249
intros i' hi',
250250
change is_compact (X.basic_open i ⊓ X.basic_open i').1,
251251
rw ← Scheme.basic_open_mul,

‎src/algebraic_geometry/open_immersion.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1776,7 +1776,7 @@ lemma Scheme.open_cover.compact_space {X : Scheme} (𝒰 : X.open_cover) [finite
17761776
begin
17771777
casesI nonempty_fintype 𝒰.J,
17781778
rw [← is_compact_univ_iff, ← 𝒰.Union_range],
1779-
apply compact_Union,
1779+
apply is_compact_Union,
17801780
intro i,
17811781
rw is_compact_iff_compact_space,
17821782
exact @@homeomorph.compact_space _ _ (H i)

‎src/algebraic_geometry/prime_spectrum/basic.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -787,7 +787,7 @@ end basic_open
787787

788788
/-- The prime spectrum of a commutative ring is a compact topological space. -/
789789
instance : compact_space (prime_spectrum R) :=
790-
{ compact_univ := by { convert is_compact_basic_open (1 : R), rw basic_open_one, refl } }
790+
{ is_compact_univ := by { convert is_compact_basic_open (1 : R), rw basic_open_one, refl } }
791791

792792
section order
793793

‎src/analysis/convex/exposed.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -199,7 +199,7 @@ end
199199

200200
protected lemma is_compact [order_closed_topology 𝕜] [t2_space E] (hAB : is_exposed 𝕜 A B)
201201
(hA : is_compact A) : is_compact B :=
202-
compact_of_is_closed_subset hA (hAB.is_closed hA.is_closed) hAB.subset
202+
is_compact_of_is_closed_subset hA (hAB.is_closed hA.is_closed) hAB.subset
203203

204204
end is_exposed
205205

‎src/analysis/convex/krein_milman.lean‎

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -65,7 +65,7 @@ begin
6565
rwa ←eq_singleton_iff_unique_mem.2 ⟨hxt, λ y hyB, _⟩,
6666
by_contra hyx,
6767
obtain ⟨l, hl⟩ := geometric_hahn_banach_point_point hyx,
68-
obtain ⟨z, hzt, hz⟩ := (compact_of_is_closed_subset hscomp htclos hst.1).exists_forall_ge
68+
obtain ⟨z, hzt, hz⟩ := (is_compact_of_is_closed_subset hscomp htclos hst.1).exists_forall_ge
6969
⟨x, hxt⟩ l.continuous.continuous_on,
7070
have h : is_exposed ℝ t {z ∈ t | ∀ w ∈ t, l w ≤ l z} := λ h, ⟨l, rfl⟩,
7171
rw ←hBmin {z ∈ t | ∀ w ∈ t, l w ≤ l z} ⟨⟨z, hzt, hz⟩, h.is_closed htclos, hst.trans
@@ -79,7 +79,8 @@ begin
7979
haveI : nonempty ↥F := hFnemp.to_subtype,
8080
rw sInter_eq_Inter,
8181
refine is_compact.nonempty_Inter_of_directed_nonempty_compact_closed _ (λ t u, _)
82-
(λ t, (hFS t.mem).1) (λ t, compact_of_is_closed_subset hscomp (hFS t.mem).2.1 (hFS t.mem).2.2.1)
82+
(λ t, (hFS t.mem).1)
83+
(λ t, is_compact_of_is_closed_subset hscomp (hFS t.mem).2.1 (hFS t.mem).2.2.1)
8384
(λ t, (hFS t.mem).2.1),
8485
obtain htu | hut := hF.total t.mem u.mem,
8586
exacts [⟨t, subset.rfl, htu⟩, ⟨u, hut, subset.rfl⟩],

‎src/analysis/convex/topology.lean‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -72,8 +72,8 @@ lemma is_closed_std_simplex : is_closed (std_simplex ℝ ι) :=
7272
(is_closed_eq (continuous_finset_sum _ $ λ x _, continuous_apply x) continuous_const)
7373

7474
/-- `std_simplex ℝ ι` is compact. -/
75-
lemma compact_std_simplex : is_compact (std_simplex ℝ ι) :=
76-
metric.compact_iff_closed_bounded.2 ⟨is_closed_std_simplex ι, bounded_std_simplex ι⟩
75+
lemma is_compact_std_simplex : is_compact (std_simplex ℝ ι) :=
76+
metric.is_compact_iff_is_closed_bounded.2 ⟨is_closed_std_simplex ι, bounded_std_simplex ι⟩
7777

7878
end std_simplex
7979

@@ -216,7 +216,7 @@ lemma set.finite.compact_convex_hull {s : set E} (hs : s.finite) :
216216
is_compact (convex_hull ℝ s) :=
217217
begin
218218
rw [hs.convex_hull_eq_image],
219-
apply (compact_std_simplex _).image,
219+
apply (is_compact_std_simplex _).image,
220220
haveI := hs.fintype,
221221
apply linear_map.continuous_on_pi
222222
end

0 commit comments

Comments
 (0)