-
Notifications
You must be signed in to change notification settings - Fork 310
/
Defs.lean
122 lines (89 loc) · 4.25 KB
/
Defs.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
/-
Copyright (c) 2022 Yury Kudryashov. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yury Kudryashov
! This file was ported from Lean 3 source module data.countable.defs
! leanprover-community/mathlib commit 70d50ecfd4900dd6d328da39ab7ebd516abe4025
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.Finite.Defs
import Mathlib.Tactic.MkIffOfInductiveProp
/-!
# Countable types
In this file we define a typeclass saying that a given `Sort _` is countable. See also `Encodable`
for a version that singles out a specific encoding of elements of `α` by natural numbers.
This file also provides a few instances of this typeclass. More instances can be found in other
files.
-/
open Function
universe u v
variable {α : Sort u} {β : Sort v}
/-!
### Definition and basic properties
-/
/-- A type `α` is countable if there exists an injective map `α → ℕ`. -/
@[mk_iff countable_iff_exists_injective]
class Countable (α : Sort u) : Prop where
/-- A type `α` is countable if there exists an injective map `α → ℕ`. -/
exists_injective_nat' : ∃ f : α → ℕ, Injective f
#align countable Countable
#align countable_iff_exists_injective countable_iff_exists_injective
lemma Countable.exists_injective_nat (α : Sort u) [Countable α] :
∃ f : α → ℕ, Injective f :=
Countable.exists_injective_nat'
instance : Countable ℕ :=
⟨⟨id, injective_id⟩⟩
export Countable (exists_injective_nat)
protected theorem Function.Injective.countable [Countable β] {f : α → β} (hf : Injective f) :
Countable α :=
let ⟨g, hg⟩ := exists_injective_nat β
⟨⟨g ∘ f, hg.comp hf⟩⟩
#align function.injective.countable Function.Injective.countable
protected theorem Function.Surjective.countable [Countable α] {f : α → β} (hf : Surjective f) :
Countable β :=
(injective_surjInv hf).countable
#align function.surjective.countable Function.Surjective.countable
theorem exists_surjective_nat (α : Sort u) [Nonempty α] [Countable α] : ∃ f : ℕ → α, Surjective f :=
let ⟨f, hf⟩ := exists_injective_nat α
⟨invFun f, invFun_surjective hf⟩
#align exists_surjective_nat exists_surjective_nat
theorem countable_iff_exists_surjective [Nonempty α] : Countable α ↔ ∃ f : ℕ → α, Surjective f :=
⟨@exists_surjective_nat _ _, fun ⟨_, hf⟩ ↦ hf.countable⟩
#align countable_iff_exists_surjective countable_iff_exists_surjective
theorem Countable.of_equiv (α : Sort _) [Countable α] (e : α ≃ β) : Countable β :=
e.symm.injective.countable
#align countable.of_equiv Countable.of_equiv
theorem Equiv.countable_iff (e : α ≃ β) : Countable α ↔ Countable β :=
⟨fun h => @Countable.of_equiv _ _ h e, fun h => @Countable.of_equiv _ _ h e.symm⟩
#align equiv.countable_iff Equiv.countable_iff
instance {β : Type v} [Countable β] : Countable (ULift.{u} β) :=
Countable.of_equiv _ Equiv.ulift.symm
/-!
### Operations on `Sort _`s
-/
instance [Countable α] : Countable (PLift α) :=
Equiv.plift.injective.countable
instance (priority := 100) Subsingleton.to_countable [Subsingleton α] : Countable α :=
⟨⟨fun _ => 0, fun x y _ => Subsingleton.elim x y⟩⟩
instance (priority := 500) Subtype.countable [Countable α] {p : α → Prop} :
Countable { x // p x } :=
Subtype.val_injective.countable
instance {n : ℕ} : Countable (Fin n) :=
Function.Injective.countable (@Fin.eq_of_veq n)
instance (priority := 100) Finite.to_countable [Finite α] : Countable α :=
let ⟨_, ⟨e⟩⟩ := Finite.exists_equiv_fin α
Countable.of_equiv _ e.symm
instance : Countable PUnit.{u} :=
Subsingleton.to_countable
instance (priority := 100) Prop.countable (p : Prop) : Countable p :=
Subsingleton.to_countable
instance Bool.countable : Countable Bool :=
⟨⟨fun b => cond b 0 1, Bool.injective_iff.2 Nat.one_ne_zero⟩⟩
instance Prop.countable' : Countable Prop :=
Countable.of_equiv Bool Equiv.propEquivBool.symm
instance (priority := 500) Quotient.countable [Countable α] {r : α → α → Prop} :
Countable (Quot r) :=
(surjective_quot_mk r).countable
instance (priority := 500) [Countable α] {s : Setoid α} : Countable (Quotient s) :=
(inferInstance : Countable (@Quot α _))