Documentation

Mathlib.Init.Set

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_1} (a : α) (s : Set α) :

      Membership in a set

      Equations
      Instances For
        instance Set.instMembership {α : Type u_1} :
        Membership α (Set α)
        Equations
        • Set.instMembership = { mem := Set.Mem }
        theorem Set.ext {α : Type u_1} {a : Set α} {b : Set α} (h : ∀ (x : α), x a x b) :
        a = b
        def Set.Subset {α : Type u_1} (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_1} :
          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_1} :
          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_1} :
                      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_1} (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_1} :
                          Insert α (Set α)
                          Equations
                          • Set.instInsert = { insert := Set.insert }
                          def Set.singleton {α : Type u_1} (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_1} :
                            Singleton α (Set α)
                            Equations
                            • Set.instSingletonSet = { singleton := Set.singleton }
                            def Set.union {α : Type u_1} (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_1} :
                              Union (Set α)
                              Equations
                              • Set.instUnion = { union := Set.union }
                              def Set.inter {α : Type u_1} (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_1} :
                                Inter (Set α)
                                Equations
                                • Set.instInter = { inter := Set.inter }
                                def Set.compl {α : Type u_1} (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_1} (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_1} :
                                    SDiff (Set α)
                                    Equations
                                    • Set.instSDiff = { sdiff := Set.diff }
                                    def Set.powerset {α : Type u_1} (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_1} {β : Type u_2} (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_1} (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