Documentation

Mathlib.Data.Set.Defs

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 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 }

          Set builder syntax. This can be elaborated to either a Set or a Finset depending on context.

          The elaborators for this syntax are located in:

          • Data.Set.Defs for the Set builder notation elaborator for syntax of the form {x | p x}, {x : α | p x}, {binder x | p x}.
          • Data.Finset.Basic for the Finset builder notation elaborator for syntax of the form {x ∈ s | p x}.
          • Data.Fintype.Basic for the Finset builder notation elaborator for syntax of the form {x | p x}, {x : α | p x}, {x ∉ s | p x}, {x ≠ a | p x}.
          • Order.LocallyFinite.Basic for the Finset builder notation elaborator for syntax of the form {x ≤ a | p x}, {x ≥ a | p x}, {x < a | p x}, {x > a | p x}.
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For

            Elaborate set builder notation for Set.

            • {x | p x} is elaborated as Set.setOf fun x ↦ p x

            • {x : α | p x} is elaborated as Set.setOf fun x : α ↦ p x

            • {binder x | p x}, where x is bound by the binder binder, is elaborated as {x | binder x ∧ p x}. The typical example is {x ∈ s | p x}, which is elaborated as {x | x ∈ s ∧ p x}. The possible binders are

              • · ∈ s, · ∉ s
              • · ⊆ s, · ⊂ s, · ⊇ s, · ⊃ s
              • · ≤ a, · ≥ a, · < a, · > a, · ≠ a

              More binders can be declared using the binder_predicate command, see Init.BinderPredicates for more info.

            See also

            • Data.Finset.Basic for the Finset builder notation elaborator partly overriding this one for syntax of the form {x ∈ s | p x}.
            • Data.Fintype.Basic for the Finset builder notation elaborator partly overriding this one for syntax of the form {x | p x}, {x : α | p x}, {x ∉ s | p x}, {x ≠ a | p x}.
            • Order.LocallyFinite.Basic for the Finset builder notation elaborator partly overriding this one for syntax of the form {x ≤ a | p x}, {x ≥ a | p x}, {x < a | p x}, {x > a | p x}.
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For

              Unexpander for set builder notation.

              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