Documentation

Mathlib.Init.Set

Note about Mathlib/Init/ #

The files in Mathlib/Init are leftovers from the port from Mathlib3. (They contain content moved from lean3 itself that Mathlib needed but was not moved to lean4.)

We intend to move all the content of these files out into the main Mathlib directory structure. Contributions assisting with this are appreciated.

Sets #

This file sets up the theory of sets whose elements have a given type.

Main definitions #

Given a type X and a predicate p : X → Prop:

Implementation issues #

As in Lean 3, Set X := X → Prop

I didn't call this file Data.Set.Basic because it contains core Lean 3 stuff which happens before mathlib3's data.set.basic . This file is a port of the core Lean 3 file lib/lean/library/init/data/set.lean.

def Set (α : Type u) :

A set is a collection of elements of some type α.

Although Set is defined as α → Prop, this is an implementation detail which should not be relied on. Instead, setOf and membership of a set () should be used to convert between sets and predicates.

Equations
Instances For
    def setOf {α : Type u} (p : αProp) :
    Set α

    Turn a predicate p : α → Prop into a set, also written as {x | p x}

    Equations
    Instances For
      def Set.Mem {α : Type u} (a : α) (s : Set α) :

      Membership in a set

      Equations
      Instances For
        instance Set.instMembership {α : Type u} :
        Membership α (Set α)
        Equations
        • Set.instMembership = { mem := Set.Mem }
        theorem Set.ext {α : Type u} {a : Set α} {b : Set α} (h : ∀ (x : α), x a x b) :
        a = b
        def Set.Subset {α : Type u} (s₁ : Set α) (s₂ : Set α) :

        The subset relation on sets. s ⊆ t means that all elements of s are elements of t.

        Note that you should not use this definition directly, but instead write s ⊆ t.

        Equations
        • s₁.Subset s₂ = ∀ ⦃a : α⦄, a s₁a s₂
        Instances For
          instance Set.instLE {α : Type u} :
          LE (Set α)

          Porting note: we introduce before to help the unifier when applying lattice theorems to subset hypotheses.

          Equations
          • Set.instLE = { le := Set.Subset }
          instance Set.instHasSubset {α : Type u} :
          Equations
          • Set.instHasSubset = { Subset := fun (x x_1 : Set α) => x x_1 }
          Equations
          • Set.instEmptyCollection = { emptyCollection := fun (x : α) => False }
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For

              { f x y | (x : X) (y : Y) } is notation for the set of elements f x y constructed from the binders x and y, equivalent to {z : Z | ∃ x y, f x y = z}.

              If f x y is a single identifier, it must be parenthesized to avoid ambiguity with {x | p x}; for instance, {(x) | (x : Nat) (y : Nat) (_hxy : x = y^2)}.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                • { pat : X | p } is notation for pattern matching in set-builder notation, where pat is a pattern that is matched by all objects of type X and p is a proposition that can refer to variables in the pattern. It is the set of all objects of type X which, when matched with the pattern pat, make p come out true.
                • { pat | p } is the same, but in the case when the type X can be inferred.

                For example, { (m, n) : ℕ × ℕ | m * n = 12 } denotes the set of all ordered pairs of natural numbers whose product is 12.

                Note that if the type ascription is left out and p can be interpreted as an extended binder, then the extended binder interpretation will be used. For example, { n + 1 | n < 3 } will be interpreted as { x : Nat | ∃ n < 3, n + 1 = x } rather than using pattern matching.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  • { pat : X | p } is notation for pattern matching in set-builder notation, where pat is a pattern that is matched by all objects of type X and p is a proposition that can refer to variables in the pattern. It is the set of all objects of type X which, when matched with the pattern pat, make p come out true.
                  • { pat | p } is the same, but in the case when the type X can be inferred.

                  For example, { (m, n) : ℕ × ℕ | m * n = 12 } denotes the set of all ordered pairs of natural numbers whose product is 12.

                  Note that if the type ascription is left out and p can be interpreted as an extended binder, then the extended binder interpretation will be used. For example, { n + 1 | n < 3 } will be interpreted as { x : Nat | ∃ n < 3, n + 1 = x } rather than using pattern matching.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For

                    Pretty printing for set-builder notation with pattern matching.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      def Set.univ {α : Type u} :
                      Set α

                      The universal set on a type α is the set containing all elements of α.

                      This is conceptually the "same as" α (in set theory, it is actually the same), but type theory makes the distinction that α is a type while Set.univ is a term of type Set α. Set.univ can itself be coerced to a type ↥Set.univ which is in bijection with (but distinct from) α.

                      Equations
                      • Set.univ = {_a : α | True}
                      Instances For
                        def Set.insert {α : Type u} (a : α) (s : Set α) :
                        Set α

                        Set.insert a s is the set {a} ∪ s.

                        Note that you should not use this definition directly, but instead write insert a s (which is mediated by the Insert typeclass).

                        Equations
                        Instances For
                          instance Set.instInsert {α : Type u} :
                          Insert α (Set α)
                          Equations
                          • Set.instInsert = { insert := Set.insert }
                          def Set.singleton {α : Type u} (a : α) :
                          Set α

                          The singleton of an element a is the set with a as a single element.

                          Note that you should not use this definition directly, but instead write {a}.

                          Equations
                          Instances For
                            instance Set.instSingletonSet {α : Type u} :
                            Singleton α (Set α)
                            Equations
                            • Set.instSingletonSet = { singleton := Set.singleton }
                            def Set.union {α : Type u} (s₁ : Set α) (s₂ : Set α) :
                            Set α

                            The union of two sets s and t is the set of elements contained in either s or t.

                            Note that you should not use this definition directly, but instead write s ∪ t.

                            Equations
                            • s₁.union s₂ = {a : α | a s₁ a s₂}
                            Instances For
                              instance Set.instUnion {α : Type u} :
                              Union (Set α)
                              Equations
                              • Set.instUnion = { union := Set.union }
                              def Set.inter {α : Type u} (s₁ : Set α) (s₂ : Set α) :
                              Set α

                              The intersection of two sets s and t is the set of elements contained in both s and t.

                              Note that you should not use this definition directly, but instead write s ∩ t.

                              Equations
                              • s₁.inter s₂ = {a : α | a s₁ a s₂}
                              Instances For
                                instance Set.instInter {α : Type u} :
                                Inter (Set α)
                                Equations
                                • Set.instInter = { inter := Set.inter }
                                def Set.compl {α : Type u} (s : Set α) :
                                Set α

                                The complement of a set s is the set of elements not contained in s.

                                Note that you should not use this definition directly, but instead write sᶜ.

                                Equations
                                • s.compl = {a : α | ¬a s}
                                Instances For
                                  def Set.diff {α : Type u} (s : Set α) (t : Set α) :
                                  Set α

                                  The difference of two sets s and t is the set of elements contained in s but not in t.

                                  Note that you should not use this definition directly, but instead write s \ t.

                                  Equations
                                  Instances For
                                    instance Set.instSDiff {α : Type u} :
                                    SDiff (Set α)
                                    Equations
                                    • Set.instSDiff = { sdiff := Set.diff }
                                    def Set.powerset {α : Type u} (s : Set α) :
                                    Set (Set α)

                                    𝒫 s is the set of all subsets of s.

                                    Equations
                                    Instances For

                                      𝒫 s is the set of all subsets of s.

                                      Equations
                                      Instances For
                                        def Set.image {α : Type u} {β : Type v} (f : αβ) (s : Set α) :
                                        Set β

                                        The image of s : Set α by f : α → β, written f '' s, is the set of b : β such that f a = b for some a ∈ s.

                                        Equations
                                        Instances For
                                          Equations
                                          def Set.Nonempty {α : Type u} (s : Set α) :

                                          The property s.Nonempty expresses the fact that the set s is not empty. It should be used in theorem assumptions instead of ∃ x, x ∈ s or s ≠ ∅ as it gives access to a nice API thanks to the dot notation.

                                          Equations
                                          • s.Nonempty = ∃ (x : α), x s
                                          Instances For