Documentation

Mathlib.Data.Set.Countable

Countable sets #

In this file we define Set.Countable s as Countable s and prove basic properties of this definition.

Note that this definition does not provide a computable encoding. For a noncomputable conversion to Encodable s, use Set.Countable.nonempty_encodable.

Keywords #

sets, countable set

def Set.Countable {α : Type u} (s : Set α) :

A set s is countable if the corresponding subtype is countable, i.e., there exists an injective map f : s → ℕ.

Note that this is an abbreviation, so hs : Set.Countable s in the proof context is the same as an instance Countable s. For a constructive version, see Encodable.

Equations
Instances For
    @[simp]
    theorem Set.countable_coe_iff {α : Type u} {s : Set α} :
    Countable s s.Countable
    theorem Set.to_countable {α : Type u} (s : Set α) [Countable s] :
    s.Countable

    Prove Set.Countable from a Countable instance on the subtype.

    theorem Countable.to_set {α : Type u} {s : Set α} :
    Countable ss.Countable

    Restate Set.Countable as a Countable instance.

    theorem Set.Countable.to_subtype {α : Type u} {s : Set α} :
    s.CountableCountable s

    Restate Set.Countable as a Countable instance.

    theorem Set.countable_iff_exists_injective {α : Type u} {s : Set α} :
    s.Countable ∃ (f : s), Function.Injective f
    theorem Set.countable_iff_exists_injOn {α : Type u} {s : Set α} :
    s.Countable ∃ (f : α), Set.InjOn f s

    A set s : Set α is countable if and only if there exists a function α → ℕ injective on s.

    theorem Set.countable_iff_nonempty_encodable {α : Type u} {s : Set α} :
    s.Countable Nonempty (Encodable s)
    theorem Set.Countable.nonempty_encodable {α : Type u} {s : Set α} :
    s.CountableNonempty (Encodable s)

    Alias of the forward direction of Set.countable_iff_nonempty_encodable.

    def Set.Countable.toEncodable {α : Type u} {s : Set α} (hs : s.Countable) :

    Convert Set.Countable s to Encodable s (noncomputable).

    Equations
    Instances For
      def Set.enumerateCountable {α : Type u} {s : Set α} (h : s.Countable) (default : α) :
      α

      Noncomputably enumerate elements in a set. The default value is used to extend the domain to all of .

      Equations
      Instances For
        theorem Set.subset_range_enumerate {α : Type u} {s : Set α} (h : s.Countable) (default : α) :
        theorem Set.range_enumerateCountable_subset {α : Type u} {s : Set α} (h : s.Countable) (default : α) :
        theorem Set.range_enumerateCountable_of_mem {α : Type u} {s : Set α} (h : s.Countable) {default : α} (h_mem : default s) :
        theorem Set.enumerateCountable_mem {α : Type u} {s : Set α} (h : s.Countable) {default : α} (h_mem : default s) (n : ) :
        theorem Set.Countable.mono {α : Type u} {s₁ : Set α} {s₂ : Set α} (h : s₁ s₂) (hs : s₂.Countable) :
        s₁.Countable
        theorem Set.countable_range {β : Type v} {ι : Sort x} [Countable ι] (f : ιβ) :
        (Set.range f).Countable
        theorem Set.countable_iff_exists_subset_range {α : Type u} [Nonempty α] {s : Set α} :
        s.Countable ∃ (f : α), s Set.range f
        theorem Set.countable_iff_exists_surjective {α : Type u} {s : Set α} (hs : s.Nonempty) :
        s.Countable ∃ (f : s), Function.Surjective f

        A non-empty set is countable iff there exists a surjection from the natural numbers onto the subtype induced by the set.

        theorem Set.Countable.exists_surjective {α : Type u} {s : Set α} (hs : s.Nonempty) :
        s.Countable∃ (f : s), Function.Surjective f

        Alias of the forward direction of Set.countable_iff_exists_surjective.


        A non-empty set is countable iff there exists a surjection from the natural numbers onto the subtype induced by the set.

        theorem Set.countable_univ {α : Type u} [Countable α] :
        Set.univ.Countable
        theorem Set.countable_univ_iff {α : Type u} :
        Set.univ.Countable Countable α
        theorem Set.Countable.exists_eq_range {α : Type u} {s : Set α} (hc : s.Countable) (hs : s.Nonempty) :
        ∃ (f : α), s = Set.range f

        If s : Set α is a nonempty countable set, then there exists a map f : ℕ → α such that s = range f.

        @[simp]
        theorem Set.countable_empty {α : Type u} :
        .Countable
        @[simp]
        theorem Set.countable_singleton {α : Type u} (a : α) :
        {a}.Countable
        theorem Set.Countable.image {α : Type u} {β : Type v} {s : Set α} (hs : s.Countable) (f : αβ) :
        (f '' s).Countable
        theorem Set.MapsTo.countable_of_injOn {α : Type u} {β : Type v} {s : Set α} {t : Set β} {f : αβ} (hf : Set.MapsTo f s t) (hf' : Set.InjOn f s) (ht : t.Countable) :
        s.Countable
        theorem Set.Countable.preimage_of_injOn {α : Type u} {β : Type v} {s : Set β} (hs : s.Countable) {f : αβ} (hf : Set.InjOn f (f ⁻¹' s)) :
        (f ⁻¹' s).Countable
        theorem Set.Countable.preimage {α : Type u} {β : Type v} {s : Set β} (hs : s.Countable) {f : αβ} (hf : Function.Injective f) :
        (f ⁻¹' s).Countable
        theorem Set.exists_seq_iSup_eq_top_iff_countable {α : Type u} [CompleteLattice α] {p : αProp} (h : ∃ (x : α), p x) :
        (∃ (s : α), (∀ (n : ), p (s n)) ⨆ (n : ), s n = ) ∃ (S : Set α), S.Countable (∀ sS, p s) sSup S =
        theorem Set.exists_seq_cover_iff_countable {α : Type u} {p : Set αProp} (h : ∃ (s : Set α), p s) :
        (∃ (s : Set α), (∀ (n : ), p (s n)) ⋃ (n : ), s n = Set.univ) ∃ (S : Set (Set α)), S.Countable (∀ sS, p s) ⋃₀ S = Set.univ
        theorem Set.countable_of_injective_of_countable_image {α : Type u} {β : Type v} {s : Set α} {f : αβ} (hf : Set.InjOn f s) (hs : (f '' s).Countable) :
        s.Countable
        theorem Set.countable_iUnion {α : Type u} {ι : Sort x} {t : ιSet α} [Countable ι] (ht : ∀ (i : ι), (t i).Countable) :
        (⋃ (i : ι), t i).Countable
        @[simp]
        theorem Set.countable_iUnion_iff {α : Type u} {ι : Sort x} [Countable ι] {t : ιSet α} :
        (⋃ (i : ι), t i).Countable ∀ (i : ι), (t i).Countable
        theorem Set.Countable.biUnion_iff {α : Type u} {β : Type v} {s : Set α} {t : (a : α) → a sSet β} (hs : s.Countable) :
        (⋃ (a : α), ⋃ (h : a s), t a h).Countable ∀ (a : α) (ha : a s), (t a ha).Countable
        theorem Set.Countable.sUnion_iff {α : Type u} {s : Set (Set α)} (hs : s.Countable) :
        (⋃₀ s).Countable as, a.Countable
        theorem Set.Countable.biUnion {α : Type u} {β : Type v} {s : Set α} {t : (a : α) → a sSet β} (hs : s.Countable) :
        (∀ (a : α) (ha : a s), (t a ha).Countable)(⋃ (a : α), ⋃ (h : a s), t a h).Countable

        Alias of the reverse direction of Set.Countable.biUnion_iff.

        theorem Set.Countable.sUnion {α : Type u} {s : Set (Set α)} (hs : s.Countable) :
        (∀ as, a.Countable)(⋃₀ s).Countable

        Alias of the reverse direction of Set.Countable.sUnion_iff.

        @[simp]
        theorem Set.countable_union {α : Type u} {s : Set α} {t : Set α} :
        (s t).Countable s.Countable t.Countable
        theorem Set.Countable.union {α : Type u} {s : Set α} {t : Set α} (hs : s.Countable) (ht : t.Countable) :
        (s t).Countable
        theorem Set.Countable.of_diff {α : Type u} {s : Set α} {t : Set α} (h : (s \ t).Countable) (ht : t.Countable) :
        s.Countable
        @[simp]
        theorem Set.countable_insert {α : Type u} {s : Set α} {a : α} :
        (insert a s).Countable s.Countable
        theorem Set.Countable.insert {α : Type u} {s : Set α} (a : α) (h : s.Countable) :
        (insert a s).Countable
        theorem Set.Finite.countable {α : Type u} {s : Set α} (hs : s.Finite) :
        s.Countable
        theorem Set.Countable.of_subsingleton {α : Type u} [Subsingleton α] (s : Set α) :
        s.Countable
        theorem Set.Subsingleton.countable {α : Type u} {s : Set α} (hs : s.Subsingleton) :
        s.Countable
        theorem Set.countable_isTop (α : Type u_1) [PartialOrder α] :
        {x : α | IsTop x}.Countable
        theorem Set.countable_isBot (α : Type u_1) [PartialOrder α] :
        {x : α | IsBot x}.Countable
        theorem Set.countable_setOf_finite_subset {α : Type u} {s : Set α} (hs : s.Countable) :
        {t : Set α | t.Finite t s}.Countable

        The set of finite subsets of a countable set is countable.

        theorem Set.Countable.setOf_finite {α : Type u} [Countable α] :
        {s : Set α | s.Finite}.Countable

        The set of finite sets in a countable type is countable.

        theorem Set.countable_univ_pi {α : Type u} {π : αType u_1} [Finite α] {s : (a : α) → Set (π a)} (hs : ∀ (a : α), (s a).Countable) :
        (Set.univ.pi s).Countable
        theorem Set.countable_pi {α : Type u} {π : αType u_1} [Finite α] {s : (a : α) → Set (π a)} (hs : ∀ (a : α), (s a).Countable) :
        {f : (a : α) → π a | ∀ (a : α), f a s a}.Countable
        theorem Set.Countable.prod {α : Type u} {β : Type v} {s : Set α} {t : Set β} (hs : s.Countable) (ht : t.Countable) :
        (s ×ˢ t).Countable
        theorem Set.Countable.image2 {α : Type u} {β : Type v} {γ : Type w} {s : Set α} {t : Set β} (hs : s.Countable) (ht : t.Countable) (f : αβγ) :
        (Set.image2 f s t).Countable
        theorem Set.countable_setOf_nonempty_of_disjoint {α : Type u} {β : Type v} {f : βSet α} (hf : Pairwise (Disjoint on f)) {s : Set α} (h'f : ∀ (t : β), f t s) (hs : s.Countable) :
        {t : β | (f t).Nonempty}.Countable

        If a family of disjoint sets is included in a countable set, then only countably many of them are nonempty.

        theorem Finset.countable_toSet {α : Type u} (s : Finset α) :
        (↑s).Countable