Documentation

Mathlib.Data.Set.Operations

Basic definitions about sets #

In this file we define various operations on sets. We also provide basic lemmas needed to unfold the definitions. More advanced theorems about these definitions are located in other files in Mathlib/Data/Set.

Main definitions #

Notations #

Keywords #

set, image, preimage

theorem Set.ext_iff {α : Type u} {a : Set α} {b : Set α} :
a = b ∀ (x : α), x a x b
@[simp]
theorem Set.mem_setOf_eq {α : Type u} {x : α} {p : αProp} :
(x {y : α | p y}) = p x
@[simp]
theorem Set.mem_univ {α : Type u} (x : α) :
x Set.univ
instance Set.instHasCompl {α : Type u} :
Equations
  • Set.instHasCompl = { compl := fun (s : Set α) => {x : α | ¬x s} }
@[simp]
theorem Set.mem_compl_iff {α : Type u} (s : Set α) (x : α) :
x s ¬x s
theorem Set.diff_eq {α : Type u} (s : Set α) (t : Set α) :
s \ t = s t
@[simp]
theorem Set.mem_diff {α : Type u} {s : Set α} {t : Set α} (x : α) :
x s \ t x s ¬x t
theorem Set.mem_diff_of_mem {α : Type u} {s : Set α} {t : Set α} {x : α} (h1 : x s) (h2 : ¬x t) :
x s \ t
@[reducible]
def Set.Elem {α : Type u} (s : Set α) :

Given the set s, Elem s is the Type of element of s.

Equations
  • s = { x : α // x s }
Instances For
    instance Set.instCoeSortType {α : Type u} :
    CoeSort (Set α) (Type u)

    Coercion from a set to the corresponding subtype.

    Equations
    • Set.instCoeSortType = { coe := Set.Elem }
    def Set.preimage {α : Type u} {β : Type v} (f : αβ) (s : Set β) :
    Set α

    The preimage of s : Set β by f : α → β, written f ⁻¹' s, is the set of x : α such that f x ∈ s.

    Equations
    Instances For

      f ⁻¹' t denotes the preimage of t : Set β under the function f : α → β.

      Equations
      Instances For
        @[simp]
        theorem Set.mem_preimage {α : Type u} {β : Type v} {f : αβ} {s : Set β} {a : α} :
        a f ⁻¹' s f a s

        f '' s denotes the image of s : Set α under the function f : α → β.

        Equations
        Instances For
          @[simp]
          theorem Set.mem_image {α : Type u} {β : Type v} (f : αβ) (s : Set α) (y : β) :
          y f '' s ∃ (x : α), x s f x = y
          theorem Set.mem_image_of_mem {α : Type u} {β : Type v} (f : αβ) {x : α} {a : Set α} (h : x a) :
          f x f '' a
          def Set.imageFactorization {α : Type u} {β : Type v} (f : αβ) (s : Set α) :
          s(f '' s)

          Restriction of f to s factors through s.imageFactorization f : s → f '' s.

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

            kernImage f s is the set of y such that f ⁻¹ y ⊆ s.

            Equations
            Instances For
              theorem Set.subset_kernImage_iff {α : Type u} {β : Type v} {s : Set β} {t : Set α} {f : αβ} :
              def Set.range {α : Type u} {ι : Sort u_1} (f : ια) :
              Set α

              Range of a function.

              This function is more flexible than f '' univ, as the image requires that the domain is in Type and not an arbitrary Sort.

              Equations
              Instances For
                @[simp]
                theorem Set.mem_range {α : Type u} {ι : Sort u_1} {f : ια} {x : α} :
                x Set.range f ∃ (y : ι), f y = x
                theorem Set.mem_range_self {α : Type u} {ι : Sort u_1} {f : ια} (i : ι) :
                def Set.rangeFactorization {α : Type u} {ι : Sort u_1} (f : ια) :
                ι(Set.range f)

                Any map f : ι → α factors through a map rangeFactorization f : ι → range f.

                Equations
                Instances For
                  noncomputable def Set.rangeSplitting {α : Type u} {β : Type v} (f : αβ) :
                  (Set.range f)α

                  We can use the axiom of choice to pick a preimage for every element of range f.

                  Equations
                  Instances For
                    theorem Set.apply_rangeSplitting {α : Type u} {β : Type v} (f : αβ) (x : (Set.range f)) :
                    f (Set.rangeSplitting f x) = x
                    @[simp]
                    theorem Set.comp_rangeSplitting {α : Type u} {β : Type v} (f : αβ) :
                    f Set.rangeSplitting f = Subtype.val
                    def Set.prod {α : Type u} {β : Type v} (s : Set α) (t : Set β) :
                    Set (α × β)

                    The cartesian product Set.prod s t is the set of (a, b) such that a ∈ s and b ∈ t.

                    Equations
                    Instances For
                      @[defaultInstance 1000]
                      instance Set.instSProd {α : Type u} {β : Type v} :
                      SProd (Set α) (Set β) (Set (α × β))
                      Equations
                      • Set.instSProd = { sprod := Set.prod }
                      theorem Set.prod_eq {α : Type u} {β : Type v} (s : Set α) (t : Set β) :
                      s ×ˢ t = Prod.fst ⁻¹' s Prod.snd ⁻¹' t
                      theorem Set.mem_prod_eq {α : Type u} {β : Type v} {s : Set α} {t : Set β} {p : α × β} :
                      (p s ×ˢ t) = (p.fst s p.snd t)
                      @[simp]
                      theorem Set.mem_prod {α : Type u} {β : Type v} {s : Set α} {t : Set β} {p : α × β} :
                      p s ×ˢ t p.fst s p.snd t
                      theorem Set.prod_mk_mem_set_prod_eq {α : Type u} {β : Type v} {a : α} {b : β} {s : Set α} {t : Set β} :
                      ((a, b) s ×ˢ t) = (a s b t)
                      theorem Set.mk_mem_prod {α : Type u} {β : Type v} {a : α} {b : β} {s : Set α} {t : Set β} (ha : a s) (hb : b t) :
                      (a, b) s ×ˢ t
                      def Set.diagonal (α : Type u_1) :
                      Set (α × α)

                      diagonal α is the set of α × α consisting of all pairs of the form (a, a).

                      Equations
                      Instances For
                        theorem Set.mem_diagonal {α : Type u} (x : α) :
                        (x, x) Set.diagonal α
                        @[simp]
                        theorem Set.mem_diagonal_iff {α : Type u} {x : α × α} :
                        x Set.diagonal α x.fst = x.snd
                        def Set.offDiag {α : Type u} (s : Set α) :
                        Set (α × α)

                        The off-diagonal of a set s is the set of pairs (a, b) with a, b ∈ s and a ≠ b.

                        Equations
                        Instances For
                          @[simp]
                          theorem Set.mem_offDiag {α : Type u} {x : α × α} {s : Set α} :
                          x s.offDiag x.fst s x.snd s x.fst x.snd
                          def Set.pi {ι : Type u_1} {α : ιType u_2} (s : Set ι) (t : (i : ι) → Set (α i)) :
                          Set ((i : ι) → α i)

                          Given an index set ι and a family of sets t : Π i, Set (α i), pi s t is the set of dependent functions f : Πa, π a such that f a belongs to t a whenever a ∈ s.

                          Equations
                          • s.pi t = {f : (i : ι) → α i | ∀ (i : ι), i sf i t i}
                          Instances For
                            @[simp]
                            theorem Set.mem_pi {ι : Type u_1} {α : ιType u_2} {s : Set ι} {t : (i : ι) → Set (α i)} {f : (i : ι) → α i} :
                            f s.pi t ∀ (i : ι), i sf i t i
                            theorem Set.mem_univ_pi {ι : Type u_1} {α : ιType u_2} {t : (i : ι) → Set (α i)} {f : (i : ι) → α i} :
                            f Set.univ.pi t ∀ (i : ι), f i t i
                            def Set.EqOn {α : Type u} {β : Type v} (f₁ : αβ) (f₂ : αβ) (s : Set α) :

                            Two functions f₁ f₂ : α → β are equal on s if f₁ x = f₂ x for all x ∈ s.

                            Equations
                            • Set.EqOn f₁ f₂ s = ∀ ⦃x : α⦄, x sf₁ x = f₂ x
                            Instances For
                              def Set.MapsTo {α : Type u} {β : Type v} (f : αβ) (s : Set α) (t : Set β) :

                              MapsTo f a b means that the image of a is contained in b.

                              Equations
                              Instances For
                                theorem Set.mapsTo_image {α : Type u} {β : Type v} (f : αβ) (s : Set α) :
                                Set.MapsTo f s (f '' s)
                                theorem Set.mapsTo_preimage {α : Type u} {β : Type v} (f : αβ) (t : Set β) :
                                Set.MapsTo f (f ⁻¹' t) t
                                def Set.MapsTo.restrict {α : Type u} {β : Type v} (f : αβ) (s : Set α) (t : Set β) (h : Set.MapsTo f s t) :
                                st

                                Given a map f sending s : Set α into t : Set β, restrict domain of f to s and the codomain to t. Same as Subtype.map.

                                Equations
                                Instances For
                                  @[simp]
                                  theorem Set.restrictPreimage_coe {α : Type u} {β : Type v} (t : Set β) (f : αβ) :
                                  ∀ (a : (f ⁻¹' t)), (t.restrictPreimage f a) = f a
                                  def Set.restrictPreimage {α : Type u} {β : Type v} (t : Set β) (f : αβ) :
                                  (f ⁻¹' t)t

                                  The restriction of a function onto the preimage of a set.

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

                                    f is injective on a if the restriction of f to a is injective.

                                    Equations
                                    • Set.InjOn f s = ∀ ⦃x₁ : α⦄, x₁ s∀ ⦃x₂ : α⦄, x₂ sf x₁ = f x₂x₁ = x₂
                                    Instances For
                                      def Set.graphOn {α : Type u} {β : Type v} (f : αβ) (s : Set α) :
                                      Set (α × β)

                                      The graph of a function f : α → β on a set s.

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

                                        f is surjective from a to b if b is contained in the image of a.

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

                                          f is bijective from s to t if f is injective on s and f '' s = t.

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

                                            g is a left inverse to f on a means that g (f x) = x for all x ∈ a.

                                            Equations
                                            Instances For
                                              @[reducible, inline]
                                              abbrev Set.RightInvOn {α : Type u} {β : Type v} (f' : βα) (f : αβ) (t : Set β) :

                                              g is a right inverse to f on b if f (g x) = x for all x ∈ b.

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

                                                g is an inverse to f viewed as a map from a to b

                                                Equations
                                                Instances For
                                                  def Set.image2 {α : Type u} {β : Type v} {γ : Type w} (f : αβγ) (s : Set α) (t : Set β) :
                                                  Set γ

                                                  The image of a binary function f : α → β → γ as a function Set α → Set β → Set γ. Mathematically this should be thought of as the image of the corresponding function α × β → γ.

                                                  Equations
                                                  Instances For
                                                    @[simp]
                                                    theorem Set.mem_image2 {α : Type u} {β : Type v} {γ : Type w} {f : αβγ} {s : Set α} {t : Set β} {c : γ} :
                                                    c Set.image2 f s t ∃ (a : α), a s ∃ (b : β), b t f a b = c
                                                    theorem Set.mem_image2_of_mem {α : Type u} {β : Type v} {γ : Type w} {f : αβγ} {s : Set α} {t : Set β} {a : α} {b : β} (ha : a s) (hb : b t) :
                                                    f a b Set.image2 f s t
                                                    def Set.seq {α : Type u} {β : Type v} (s : Set (αβ)) (t : Set α) :
                                                    Set β

                                                    Given a set s of functions α → β and t : Set α, seq s t is the union of f '' t over all f ∈ s.

                                                    Equations
                                                    Instances For
                                                      @[simp]
                                                      theorem Set.mem_seq_iff {α : Type u} {β : Type v} {s : Set (αβ)} {t : Set α} {b : β} :
                                                      b s.seq t ∃ (f : αβ), f s ∃ (a : α), a t f a = b
                                                      theorem Set.seq_eq_image2 {α : Type u} {β : Type v} (s : Set (αβ)) (t : Set α) :
                                                      s.seq t = Set.image2 (fun (f : αβ) (a : α) => f a) s t