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) :
Instances For
    def setOf {α : Type u} (p : αProp) :
    Set α
    Instances For
      def Set.Mem {α : Type u_1} (a : α) (s : Set α) :

      Membership in a set

      Instances For
        instance Set.instMembershipSet {α : Type u_1} :
        Membership α (Set α)
        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 α) :
        Instances For
          instance Set.instLESet {α : Type u_1} :
          LE (Set α)

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

          instance Set.instHasSubsetSet {α : Type u_1} :
          def Set.univ {α : Type u_1} :
          Set α
          Instances For
            def Set.insert {α : Type u_1} (a : α) (s : Set α) :
            Set α
            Instances For
              instance Set.instInsertSet {α : Type u_1} :
              Insert α (Set α)
              def Set.singleton {α : Type u_1} (a : α) :
              Set α
              Instances For
                instance Set.instSingletonSet {α : Type u_1} :
                Singleton α (Set α)
                def Set.union {α : Type u_1} (s₁ : Set α) (s₂ : Set α) :
                Set α
                Instances For
                  instance Set.instUnionSet {α : Type u_1} :
                  Union (Set α)
                  def Set.inter {α : Type u_1} (s₁ : Set α) (s₂ : Set α) :
                  Set α
                  Instances For
                    instance Set.instInterSet {α : Type u_1} :
                    Inter (Set α)
                    def Set.compl {α : Type u_1} (s : Set α) :
                    Set α
                    Instances For
                      def Set.diff {α : Type u_1} (s : Set α) (t : Set α) :
                      Set α
                      Instances For
                        instance Set.instSDiffSet {α : Type u_1} :
                        SDiff (Set α)
                        def Set.powerset {α : Type u_1} (s : Set α) :
                        Set (Set α)
                        Instances For
                          def Set.image {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set α) :
                          Set β
                          Instances For