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 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 : α) :
instance Set.instHasCompl {α : Type u} :
Equations
    @[simp]
    theorem Set.mem_compl_iff {α : Type u} (s : Set α) (x : α) :
    x s ¬x s
    theorem Set.diff_eq {α : Type u} (s t : Set α) :
    s \ t = s t
    @[simp]
    theorem Set.mem_diff {α : Type u} {s t : Set α} (x : α) :
    x s \ t x s ¬x t
    theorem Set.mem_diff_of_mem {α : Type u} {s t : Set α} {x : α} (h1 : x s) (h2 : ¬x t) :
    x s \ t
    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 : αβ} :
                        s kernImage f t f ⁻¹' s t
                        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 range f (y : ι), f y = x
                            theorem Set.mem_range_self {α : Type u} {ι : Sort u_1} {f : ια} (i : ι) :
                            f i range f
                            def Set.rangeFactorization {α : Type u} {ι : Sort u_1} (f : ια) :
                            ι(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 : αβ) :
                                (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 : (range f)) :
                                    f (rangeSplitting f x) = x
                                    @[simp]
                                    theorem Set.comp_rangeSplitting {α : Type u} {β : Type v} (f : αβ) :
                                    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
                                          theorem Set.prod_eq {α : Type u} {β : Type v} (s : Set α) (t : Set β) :
                                          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.prodMk_mem_set_prod_eq {α : Type u} {β : Type v} {a : α} {b : β} {s : Set α} {t : Set β} :
                                          ((a, b) s ×ˢ t) = (a s b t)
                                          @[deprecated Set.prodMk_mem_set_prod_eq (since := "2025-02-21")]
                                          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)

                                          Alias of Set.prodMk_mem_set_prod_eq.

                                          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 : α) :
                                              @[simp]
                                              theorem Set.mem_diagonal_iff {α : Type u} {x : α × α} :
                                              x 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 i belongs to t i whenever i ∈ s.

                                                  Equations
                                                    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 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
                                                        Instances For
                                                          def Set.MapsTo {α : Type u} {β : Type v} (f : αβ) (s : Set α) (t : Set β) :

                                                          MapsTo f s t means that the image of s is contained in t.

                                                          Equations
                                                            Instances For
                                                              theorem Set.mapsTo_image {α : Type u} {β : Type v} (f : αβ) (s : Set α) :
                                                              MapsTo f s (f '' s)
                                                              theorem Set.mapsTo_preimage {α : Type u} {β : Type v} (f : αβ) (t : Set β) :
                                                              MapsTo f (f ⁻¹' t) t
                                                              def Set.MapsTo.restrict {α : Type u} {β : Type v} (f : αβ) (s : Set α) (t : Set β) (h : 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
                                                                  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
                                                                      @[simp]
                                                                      theorem Set.restrictPreimage_coe {α : Type u} {β : Type v} (t : Set β) (f : αβ) (a✝ : ↑(f ⁻¹' t)) :
                                                                      (t.restrictPreimage f a✝) = f a✝
                                                                      def Set.InjOn {α : Type u} {β : Type v} (f : αβ) (s : Set α) :

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

                                                                      Equations
                                                                        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 s to t if t is contained in the image of s.

                                                                              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} (g : βα) (f : αβ) (s : Set α) :

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

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

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

                                                                                          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 s to t

                                                                                              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 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 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 = image2 (fun (f : αβ) (a : α) => f a) s t