From 6379d39e6b5b279df9715f8011369a301b634e41 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Violeta=20Hern=C3=A1ndez?= Date: Sun, 17 Jul 2022 17:25:03 +0000 Subject: [PATCH] feat(data/set/countable): protect lemmas (#15415) We protect `set.countable_iff_exists_injective`, `set.countable_iff_exists_surjective`, and `set.countable.to_encodable` in order to avoid clashes with the theorems on the new `countable` typeclass. --- src/data/countable/basic.lean | 2 +- src/data/set/countable.lean | 10 +++++----- src/set_theory/cardinal/basic.lean | 2 +- src/topology/bases.lean | 2 +- src/topology/metric_space/kuratowski.lean | 2 +- 5 files changed, 9 insertions(+), 9 deletions(-) diff --git a/src/data/countable/basic.lean b/src/data/countable/basic.lean index eff5e9cfa86eb..9db635167cc68 100644 --- a/src/data/countable/basic.lean +++ b/src/data/countable/basic.lean @@ -10,7 +10,7 @@ import data.countable.defs /-! # Countable types -In this file we provide basis instances of the `countable` typeclass defined elsewhere. +In this file we provide basic instances of the `countable` typeclass defined elsewhere. -/ universes u v w diff --git a/src/data/set/countable.lean b/src/data/set/countable.lean index 4b490f54a46a7..29bb573f252db 100644 --- a/src/data/set/countable.lean +++ b/src/data/set/countable.lean @@ -27,7 +27,7 @@ constructive analogue of countability. (For the most part, theorems about -/ protected def countable (s : set α) : Prop := nonempty (encodable s) -lemma countable_iff_exists_injective {s : set α} : +protected lemma countable_iff_exists_injective {s : set α} : s.countable ↔ ∃f:s → ℕ, injective f := ⟨λ ⟨h⟩, by exactI ⟨encode, encode_injective⟩, λ ⟨f, h⟩, ⟨⟨f, partial_inv f, partial_inv_left h⟩⟩⟩ @@ -36,13 +36,13 @@ lemma countable_iff_exists_injective {s : set α} : on `s`. -/ lemma countable_iff_exists_inj_on {s : set α} : s.countable ↔ ∃ f : α → ℕ, inj_on f s := -countable_iff_exists_injective.trans +set.countable_iff_exists_injective.trans ⟨λ ⟨f, hf⟩, ⟨λ a, if h : a ∈ s then f ⟨a, h⟩ else 0, λ a as b bs h, congr_arg subtype.val $ hf $ by simpa [as, bs] using h⟩, λ ⟨f, hf⟩, ⟨_, inj_on_iff_injective.1 hf⟩⟩ -lemma countable_iff_exists_surjective [ne : nonempty α] {s : set α} : +protected lemma countable_iff_exists_surjective [ne : nonempty α] {s : set α} : s.countable ↔ ∃f:ℕ → α, s ⊆ range f := ⟨λ ⟨h⟩, by inhabit α; exactI ⟨λ n, ((decode s n).map subtype.val).iget, λ a as, ⟨encode (⟨a, as⟩ : s), by simp [encodek]⟩⟩, @@ -69,7 +69,7 @@ have (∃ f : ℕ → s, surjective f) → s.countable, from assume ⟨f, fsurj by split; assumption /-- Convert `set.countable s` to `encodable s` (noncomputable). -/ -def countable.to_encodable {s : set α} : s.countable → encodable s := +protected def countable.to_encodable {s : set α} : s.countable → encodable s := classical.choice lemma countable_encodable' (s : set α) [H : encodable s] : s.countable := @@ -86,7 +86,7 @@ begin letI : encodable s := countable.to_encodable hc, letI : nonempty s := hs.to_subtype, have : (univ : set s).countable := countable_encodable _, - rcases countable_iff_exists_surjective.1 this with ⟨g, hg⟩, + rcases set.countable_iff_exists_surjective.1 this with ⟨g, hg⟩, have : range g = univ := univ_subset_iff.1 hg, use coe ∘ g, simp only [range_comp, this, image_univ, subtype.range_coe] diff --git a/src/set_theory/cardinal/basic.lean b/src/set_theory/cardinal/basic.lean index 7df47fdb8529d..7be2e3c90f840 100644 --- a/src/set_theory/cardinal/basic.lean +++ b/src/set_theory/cardinal/basic.lean @@ -1038,7 +1038,7 @@ denumerable_iff.1 ⟨‹_›⟩ @[simp] lemma mk_set_le_aleph_0 (s : set α) : #s ≤ ℵ₀ ↔ s.countable := begin - rw [countable_iff_exists_injective], split, + rw [set.countable_iff_exists_injective], split, { rintro ⟨f'⟩, cases embedding.trans f' equiv.ulift.to_embedding with f hf, exact ⟨f, hf⟩ }, { rintro ⟨f, hf⟩, exact ⟨embedding.trans ⟨f, hf⟩ equiv.ulift.symm.to_embedding⟩ } end diff --git a/src/topology/bases.lean b/src/topology/bases.lean index 2f50a653cfc17..79046cc2004a6 100644 --- a/src/topology/bases.lean +++ b/src/topology/bases.lean @@ -275,7 +275,7 @@ If `α` might be empty, then `exists_countable_dense` is the main way to use sep lemma exists_dense_seq [separable_space α] [nonempty α] : ∃ u : ℕ → α, dense_range u := begin obtain ⟨s : set α, hs, s_dense⟩ := exists_countable_dense α, - cases countable_iff_exists_surjective.mp hs with u hu, + cases set.countable_iff_exists_surjective.mp hs with u hu, exact ⟨u, s_dense.mono hu⟩, end diff --git a/src/topology/metric_space/kuratowski.lean b/src/topology/metric_space/kuratowski.lean index 10fdd3f0f39e4..d832d6b4cb81b 100644 --- a/src/topology/metric_space/kuratowski.lean +++ b/src/topology/metric_space/kuratowski.lean @@ -91,7 +91,7 @@ begin haveI : inhabited α := ⟨basepoint⟩, have : ∃s:set α, s.countable ∧ dense s := exists_countable_dense α, rcases this with ⟨S, ⟨S_countable, S_dense⟩⟩, - rcases countable_iff_exists_surjective.1 S_countable with ⟨x, x_range⟩, + rcases set.countable_iff_exists_surjective.1 S_countable with ⟨x, x_range⟩, /- Use embedding_of_subset to construct the desired isometry -/ exact ⟨embedding_of_subset x, embedding_of_subset_isometry x (S_dense.mono x_range)⟩ } end