Documentation

Mathlib.Data.Set.Prod

Sets in product and pi types #

This file proves basic properties of product of sets in α × β and in Π i, α i, and of the diagonal of a type.

Main declarations #

This file contains basic results on the following notions, which are defined in Set.Operations.

Cartesian binary product of sets #

theorem Set.Subsingleton.prod {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} (hs : s.Subsingleton) (ht : t.Subsingleton) :
noncomputable instance Set.decidableMemProd {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} [DecidablePred fun (x : α) => x s] [DecidablePred fun (x : β) => x t] :
DecidablePred fun (x : α × β) => x s ×ˢ t
Equations
    theorem Set.prod_mono {α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {t₁ t₂ : Set β} (hs : s₁ s₂) (ht : t₁ t₂) :
    s₁ ×ˢ t₁ s₂ ×ˢ t₂
    theorem Set.prod_mono_left {α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {t : Set β} (hs : s₁ s₂) :
    s₁ ×ˢ t s₂ ×ˢ t
    theorem Set.prod_mono_right {α : Type u_1} {β : Type u_2} {s : Set α} {t₁ t₂ : Set β} (ht : t₁ t₂) :
    s ×ˢ t₁ s ×ˢ t₂
    @[simp]
    theorem Set.prod_self_subset_prod_self {α : Type u_1} {s₁ s₂ : Set α} :
    s₁ ×ˢ s₁ s₂ ×ˢ s₂ s₁ s₂
    @[simp]
    theorem Set.prod_self_ssubset_prod_self {α : Type u_1} {s₁ s₂ : Set α} :
    s₁ ×ˢ s₁ s₂ ×ˢ s₂ s₁ s₂
    theorem Set.prod_subset_iff {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {P : Set (α × β)} :
    s ×ˢ t P xs, yt, (x, y) P
    theorem Set.forall_prod_set {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {p : α × βProp} :
    (∀ xs ×ˢ t, p x) xs, yt, p (x, y)
    theorem Set.exists_prod_set {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {p : α × βProp} :
    (∃ xs ×ˢ t, p x) xs, yt, p (x, y)
    @[simp]
    theorem Set.prod_empty {α : Type u_1} {β : Type u_2} {s : Set α} :
    @[simp]
    theorem Set.empty_prod {α : Type u_1} {β : Type u_2} {t : Set β} :
    @[simp]
    theorem Set.univ_prod_univ {α : Type u_1} {β : Type u_2} :
    theorem Set.univ_prod {α : Type u_1} {β : Type u_2} {t : Set β} :
    theorem Set.prod_univ {α : Type u_1} {β : Type u_2} {s : Set α} :
    @[simp]
    theorem Set.prod_eq_univ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} [Nonempty α] [Nonempty β] :
    theorem Set.singleton_prod {α : Type u_1} {β : Type u_2} {t : Set β} {a : α} :
    {a} ×ˢ t = Prod.mk a '' t
    theorem Set.prod_singleton {α : Type u_1} {β : Type u_2} {s : Set α} {b : β} :
    s ×ˢ {b} = (fun (a : α) => (a, b)) '' s
    @[simp]
    theorem Set.singleton_prod_singleton {α : Type u_1} {β : Type u_2} {a : α} {b : β} :
    @[simp]
    theorem Set.union_prod {α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {t : Set β} :
    (s₁ s₂) ×ˢ t = s₁ ×ˢ t s₂ ×ˢ t
    @[simp]
    theorem Set.prod_union {α : Type u_1} {β : Type u_2} {s : Set α} {t₁ t₂ : Set β} :
    s ×ˢ (t₁ t₂) = s ×ˢ t₁ s ×ˢ t₂
    theorem Set.inter_prod {α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {t : Set β} :
    (s₁ s₂) ×ˢ t = s₁ ×ˢ t s₂ ×ˢ t
    theorem Set.prod_inter {α : Type u_1} {β : Type u_2} {s : Set α} {t₁ t₂ : Set β} :
    s ×ˢ (t₁ t₂) = s ×ˢ t₁ s ×ˢ t₂
    theorem Set.prod_inter_prod {α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {t₁ t₂ : Set β} :
    s₁ ×ˢ t₁ s₂ ×ˢ t₂ = (s₁ s₂) ×ˢ (t₁ t₂)
    theorem Set.compl_prod_eq_union {α : Type u_5} {β : Type u_6} (s : Set α) (t : Set β) :
    @[simp]
    theorem Set.disjoint_prod {α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {t₁ t₂ : Set β} :
    Disjoint (s₁ ×ˢ t₁) (s₂ ×ˢ t₂) Disjoint s₁ s₂ Disjoint t₁ t₂
    theorem Set.Disjoint.set_prod_left {α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} (hs : Disjoint s₁ s₂) (t₁ t₂ : Set β) :
    Disjoint (s₁ ×ˢ t₁) (s₂ ×ˢ t₂)
    theorem Set.Disjoint.set_prod_right {α : Type u_1} {β : Type u_2} {t₁ t₂ : Set β} (ht : Disjoint t₁ t₂) (s₁ s₂ : Set α) :
    Disjoint (s₁ ×ˢ t₁) (s₂ ×ˢ t₂)
    theorem Set.prodMap_image_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : αβ) (g : γδ) (s : Set α) (t : Set γ) :
    Prod.map f g '' s ×ˢ t = (f '' s) ×ˢ (g '' t)
    theorem Set.insert_prod {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {a : α} :
    insert a s ×ˢ t = Prod.mk a '' t s ×ˢ t
    theorem Set.prod_insert {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {b : β} :
    s ×ˢ insert b t = (fun (a : α) => (a, b)) '' s s ×ˢ t
    theorem Set.prod_preimage_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {s : Set α} {t : Set β} {f : γα} {g : δβ} :
    (f ⁻¹' s) ×ˢ (g ⁻¹' t) = (fun (p : γ × δ) => (f p.1, g p.2)) ⁻¹' s ×ˢ t
    theorem Set.prod_preimage_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {t : Set β} {f : γα} :
    (f ⁻¹' s) ×ˢ t = (fun (p : γ × β) => (f p.1, p.2)) ⁻¹' s ×ˢ t
    theorem Set.prod_preimage_right {α : Type u_1} {β : Type u_2} {δ : Type u_4} {s : Set α} {t : Set β} {g : δβ} :
    s ×ˢ (g ⁻¹' t) = (fun (p : α × δ) => (p.1, g p.2)) ⁻¹' s ×ˢ t
    theorem Set.preimage_prod_map_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : αβ) (g : γδ) (s : Set β) (t : Set δ) :
    Prod.map f g ⁻¹' s ×ˢ t = (f ⁻¹' s) ×ˢ (g ⁻¹' t)
    theorem Set.mk_preimage_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {t : Set β} (f : γα) (g : γβ) :
    (fun (x : γ) => (f x, g x)) ⁻¹' s ×ˢ t = f ⁻¹' s g ⁻¹' t
    @[simp]
    theorem Set.mk_preimage_prod_left {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {b : β} (hb : b t) :
    (fun (a : α) => (a, b)) ⁻¹' s ×ˢ t = s
    @[simp]
    theorem Set.mk_preimage_prod_right {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {a : α} (ha : a s) :
    @[simp]
    theorem Set.mk_preimage_prod_left_eq_empty {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {b : β} (hb : bt) :
    (fun (a : α) => (a, b)) ⁻¹' s ×ˢ t =
    @[simp]
    theorem Set.mk_preimage_prod_right_eq_empty {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {a : α} (ha : as) :
    theorem Set.mk_preimage_prod_left_eq_if {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {b : β} [DecidablePred fun (x : β) => x t] :
    (fun (a : α) => (a, b)) ⁻¹' s ×ˢ t = if b t then s else
    theorem Set.mk_preimage_prod_right_eq_if {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {a : α} [DecidablePred fun (x : α) => x s] :
    theorem Set.mk_preimage_prod_left_fn_eq_if {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {t : Set β} {b : β} [DecidablePred fun (x : β) => x t] (f : γα) :
    (fun (a : γ) => (f a, b)) ⁻¹' s ×ˢ t = if b t then f ⁻¹' s else
    theorem Set.mk_preimage_prod_right_fn_eq_if {α : Type u_1} {β : Type u_2} {δ : Type u_4} {s : Set α} {t : Set β} {a : α} [DecidablePred fun (x : α) => x s] (g : δβ) :
    (fun (b : δ) => (a, g b)) ⁻¹' s ×ˢ t = if a s then g ⁻¹' t else
    @[simp]
    theorem Set.preimage_swap_prod {α : Type u_1} {β : Type u_2} (s : Set α) (t : Set β) :
    @[simp]
    theorem Set.image_swap_prod {α : Type u_1} {β : Type u_2} (s : Set α) (t : Set β) :
    theorem Set.mapsTo_swap_prod {α : Type u_1} {β : Type u_2} (s : Set α) (t : Set β) :
    theorem Set.prod_image_image_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {s : Set α} {t : Set β} {m₁ : αγ} {m₂ : βδ} :
    (m₁ '' s) ×ˢ (m₂ '' t) = (fun (p : α × β) => (m₁ p.1, m₂ p.2)) '' s ×ˢ t
    theorem Set.prod_range_range_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {m₁ : αγ} {m₂ : βδ} :
    range m₁ ×ˢ range m₂ = range fun (p : α × β) => (m₁ p.1, m₂ p.2)
    @[simp]
    theorem Set.range_prodMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {m₁ : αγ} {m₂ : βδ} :
    range (Prod.map m₁ m₂) = range m₁ ×ˢ range m₂
    @[deprecated Set.range_prodMap (since := "2025-04-10")]
    theorem Set.range_prod_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {m₁ : αγ} {m₂ : βδ} :
    range (Prod.map m₁ m₂) = range m₁ ×ˢ range m₂

    Alias of Set.range_prodMap.

    theorem Set.prod_range_univ_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m₁ : αγ} :
    range m₁ ×ˢ univ = range fun (p : α × β) => (m₁ p.1, p.2)
    theorem Set.prod_univ_range_eq {α : Type u_1} {β : Type u_2} {δ : Type u_4} {m₂ : βδ} :
    univ ×ˢ range m₂ = range fun (p : α × β) => (p.1, m₂ p.2)
    theorem Set.range_pair_subset {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβ) (g : αγ) :
    (range fun (x : α) => (f x, g x)) range f ×ˢ range g
    theorem Set.Nonempty.prod {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} :
    s.Nonemptyt.Nonempty(s ×ˢ t).Nonempty
    theorem Set.Nonempty.fst {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} :
    (s ×ˢ t).Nonemptys.Nonempty
    theorem Set.Nonempty.snd {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} :
    (s ×ˢ t).Nonemptyt.Nonempty
    @[simp]
    theorem Set.prod_nonempty_iff {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} :
    @[simp]
    theorem Set.prod_eq_empty_iff {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} :
    s ×ˢ t = s = t =
    theorem Set.prod_sub_preimage_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {t : Set β} {W : Set γ} {f : α × βγ} :
    s ×ˢ t f ⁻¹' W ∀ (a : α) (b : β), a sb tf (a, b) W
    theorem Set.image_prodMk_subset_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : αβ} {g : αγ} {s : Set α} :
    (fun (x : α) => (f x, g x)) '' s (f '' s) ×ˢ (g '' s)
    @[deprecated Set.image_prodMk_subset_prod (since := "2025-02-22")]
    theorem Set.image_prod_mk_subset_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : αβ} {g : αγ} {s : Set α} :
    (fun (x : α) => (f x, g x)) '' s (f '' s) ×ˢ (g '' s)

    Alias of Set.image_prodMk_subset_prod.

    theorem Set.image_prodMk_subset_prod_left {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {b : β} (hb : b t) :
    (fun (a : α) => (a, b)) '' s s ×ˢ t
    @[deprecated Set.image_prodMk_subset_prod_left (since := "2025-02-22")]
    theorem Set.image_prod_mk_subset_prod_left {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {b : β} (hb : b t) :
    (fun (a : α) => (a, b)) '' s s ×ˢ t

    Alias of Set.image_prodMk_subset_prod_left.

    theorem Set.image_prodMk_subset_prod_right {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {a : α} (ha : a s) :
    Prod.mk a '' t s ×ˢ t
    @[deprecated Set.image_prodMk_subset_prod_right (since := "2025-02-22")]
    theorem Set.image_prod_mk_subset_prod_right {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {a : α} (ha : a s) :
    Prod.mk a '' t s ×ˢ t

    Alias of Set.image_prodMk_subset_prod_right.

    theorem Set.prod_subset_preimage_fst {α : Type u_1} {β : Type u_2} (s : Set α) (t : Set β) :
    theorem Set.fst_image_prod_subset {α : Type u_1} {β : Type u_2} (s : Set α) (t : Set β) :
    theorem Set.fst_image_prod {α : Type u_1} {β : Type u_2} (s : Set β) {t : Set α} (ht : t.Nonempty) :
    theorem Set.mapsTo_fst_prod {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} :
    theorem Set.prod_subset_preimage_snd {α : Type u_1} {β : Type u_2} (s : Set α) (t : Set β) :
    theorem Set.snd_image_prod_subset {α : Type u_1} {β : Type u_2} (s : Set α) (t : Set β) :
    theorem Set.snd_image_prod {α : Type u_1} {β : Type u_2} {s : Set α} (hs : s.Nonempty) (t : Set β) :
    theorem Set.subset_fst_image_prod_snd_image {α : Type u_1} {β : Type u_2} {s : Set (α × β)} :
    theorem Set.mapsTo_snd_prod {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} :
    theorem Set.prod_diff_prod {α : Type u_1} {β : Type u_2} {s s₁ : Set α} {t t₁ : Set β} :
    s ×ˢ t \ s₁ ×ˢ t₁ = s ×ˢ (t \ t₁) (s \ s₁) ×ˢ t
    theorem Set.prod_subset_prod_iff {α : Type u_1} {β : Type u_2} {s s₁ : Set α} {t t₁ : Set β} :
    s ×ˢ t s₁ ×ˢ t₁ s s₁ t t₁ s = t =

    A product set is included in a product set if and only factors are included, or a factor of the first set is empty.

    theorem Set.prod_eq_prod_iff_of_nonempty {α : Type u_1} {β : Type u_2} {s s₁ : Set α} {t t₁ : Set β} (h : (s ×ˢ t).Nonempty) :
    s ×ˢ t = s₁ ×ˢ t₁ s = s₁ t = t₁
    theorem Set.prod_eq_prod_iff {α : Type u_1} {β : Type u_2} {s s₁ : Set α} {t t₁ : Set β} :
    s ×ˢ t = s₁ ×ˢ t₁ s = s₁ t = t₁ (s = t = ) (s₁ = t₁ = )
    @[simp]
    theorem Set.prod_eq_iff_eq {α : Type u_1} {β : Type u_2} {s s₁ : Set α} {t : Set β} (ht : t.Nonempty) :
    s ×ˢ t = s₁ ×ˢ t s = s₁
    theorem Set.subset_prod {α : Type u_1} {β : Type u_2} {s : Set (α × β)} :
    theorem Monotone.set_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] {f : αSet β} {g : αSet γ} (hf : Monotone f) (hg : Monotone g) :
    Monotone fun (x : α) => f x ×ˢ g x
    theorem Antitone.set_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] {f : αSet β} {g : αSet γ} (hf : Antitone f) (hg : Antitone g) :
    Antitone fun (x : α) => f x ×ˢ g x
    theorem MonotoneOn.set_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} [Preorder α] {f : αSet β} {g : αSet γ} (hf : MonotoneOn f s) (hg : MonotoneOn g s) :
    MonotoneOn (fun (x : α) => f x ×ˢ g x) s
    theorem AntitoneOn.set_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} [Preorder α] {f : αSet β} {g : αSet γ} (hf : AntitoneOn f s) (hg : AntitoneOn g s) :
    AntitoneOn (fun (x : α) => f x ×ˢ g x) s

    Diagonal #

    In this section we prove some lemmas about the diagonal set {p | p.1 = p.2} and the diagonal map fun x ↦ (x, x).

    instance Set.decidableMemDiagonal {α : Type u_1} [h : DecidableEq α] (x : α × α) :
    Equations
      theorem Set.preimage_coe_coe_diagonal {α : Type u_1} (s : Set α) :
      (Prod.map (fun (x : s) => x) fun (x : s) => x) ⁻¹' diagonal α = diagonal s
      @[simp]
      theorem Set.range_diag {α : Type u_1} :
      (range fun (x : α) => (x, x)) = diagonal α
      theorem Set.diagonal_subset_iff {α : Type u_1} {s : Set (α × α)} :
      diagonal α s ∀ (x : α), (x, x) s
      @[simp]
      @[simp]
      theorem Set.diag_preimage_prod {α : Type u_1} (s t : Set α) :
      (fun (x : α) => (x, x)) ⁻¹' s ×ˢ t = s t
      theorem Set.diag_preimage_prod_self {α : Type u_1} (s : Set α) :
      (fun (x : α) => (x, x)) ⁻¹' s ×ˢ s = s
      theorem Set.diag_image {α : Type u_1} (s : Set α) :
      (fun (x : α) => (x, x)) '' s = diagonal α s ×ˢ s
      theorem Set.range_const_eq_diagonal {α : Type u_1} {β : Type u_2} [ : Nonempty β] :
      range (Function.const α) = {f : αβ | ∀ (x y : α), f x = f y}

      A function is Function.const α a for some a if and only if ∀ x y, f x = f y.

      @[reducible, inline]
      abbrev Function.Pullback {X : Type u_1} {Y : Sort u_2} {Z : Type u_3} (f : XY) (g : ZY) :
      Type (max 0 u_3 u_1)

      The fiber product $X \times_Y Z$.

      Equations
        Instances For
          @[reducible, inline]
          abbrev Function.PullbackSelf {X : Type u_1} {Y : Sort u_2} (f : XY) :
          Type u_1

          The fiber product $X \times_Y X$.

          Equations
            Instances For
              def Function.Pullback.fst {X : Type u_1} {Y : Sort u_2} {Z : Type u_3} {f : XY} {g : ZY} (p : Pullback f g) :
              X

              The projection from the fiber product to the first factor.

              Equations
                Instances For
                  def Function.Pullback.snd {X : Type u_1} {Y : Sort u_2} {Z : Type u_3} {f : XY} {g : ZY} (p : Pullback f g) :
                  Z

                  The projection from the fiber product to the second factor.

                  Equations
                    Instances For
                      theorem Function.pullback_comm_sq {X : Type u_2} {Y : Sort u_3} {Z : Type u_1} (f : XY) (g : ZY) :
                      def toPullbackDiag {X : Type u_1} {Y : Sort u_2} (f : XY) (x : X) :

                      The diagonal map $\Delta: X \to X \times_Y X$.

                      Equations
                        Instances For
                          @[simp]
                          theorem toPullbackDiag_coe {X : Type u_1} {Y : Sort u_2} (f : XY) (x : X) :
                          (toPullbackDiag f x) = (x, x)
                          def Function.pullbackDiagonal {X : Type u_1} {Y : Sort u_2} (f : XY) :

                          The diagonal $\Delta(X) \subseteq X \times_Y X$.

                          Equations
                            Instances For
                              def Function.mapPullback {X₁ : Type u_1} {X₂ : Type u_2} {Y₁ : Sort u_3} {Y₂ : Sort u_4} {Z₁ : Type u_5} {Z₂ : Type u_6} {f₁ : X₁Y₁} {g₁ : Z₁Y₁} {f₂ : X₂Y₂} {g₂ : Z₂Y₂} (mapX : X₁X₂) (mapY : Y₁Y₂) (mapZ : Z₁Z₂) (commX : f₂ mapX = mapY f₁) (commZ : g₂ mapZ = mapY g₁) (p : Pullback f₁ g₁) :
                              Pullback f₂ g₂

                              Three functions between the three pairs of spaces $X_i, Y_i, Z_i$ that are compatible induce a function $X_1 \times_{Y_1} Z_1 \to X_2 \times_{Y_2} Z_2$.

                              Equations
                                Instances For
                                  def Function.PullbackSelf.map_fst {X : Type u_1} {Y : Sort u_2} {Z : Type u_3} {f : XY} {g : ZY} :

                                  The projection $(X \times_Y Z) \times_Z (X \times_Y Z) \to X \times_Y X$.

                                  Equations
                                    Instances For
                                      def Function.PullbackSelf.map_snd {X : Type u_1} {Y : Sort u_2} {Z : Type u_3} {f : XY} {g : ZY} :

                                      The projection $(X \times_Y Z) \times_X (X \times_Y Z) \to Z \times_Y Z$.

                                      Equations
                                        Instances For
                                          theorem Function.Injective.preimage_pullbackDiagonal {X : Type u_2} {Y : Sort u_3} {Z : Type u_1} {f : XY} {g : ZX} (inj : Injective g) :
                                          theorem image_toPullbackDiag {X : Type u_1} {Y : Sort u_2} (f : XY) (s : Set X) :
                                          theorem injective_toPullbackDiag {X : Type u_1} {Y : Sort u_2} (f : XY) :
                                          @[simp]
                                          theorem Set.offDiag_nonempty {α : Type u_1} {s : Set α} :
                                          @[simp]
                                          theorem Set.offDiag_eq_empty {α : Type u_1} {s : Set α} :
                                          theorem Set.Nontrivial.offDiag_nonempty {α : Type u_1} {s : Set α} :

                                          Alias of the reverse direction of Set.offDiag_nonempty.

                                          Alias of the reverse direction of Set.offDiag_nonempty.

                                          theorem Set.offDiag_subset_prod {α : Type u_1} (s : Set α) :
                                          theorem Set.offDiag_eq_sep_prod {α : Type u_1} (s : Set α) :
                                          s.offDiag = {x : α × α | x s ×ˢ s x.1 x.2}
                                          @[simp]
                                          theorem Set.offDiag_empty {α : Type u_1} :
                                          @[simp]
                                          theorem Set.offDiag_singleton {α : Type u_1} (a : α) :
                                          @[simp]
                                          theorem Set.offDiag_univ {α : Type u_1} :
                                          @[simp]
                                          theorem Set.prod_sdiff_diagonal {α : Type u_1} (s : Set α) :
                                          @[simp]
                                          theorem Set.disjoint_diagonal_offDiag {α : Type u_1} (s : Set α) :
                                          theorem Set.offDiag_inter {α : Type u_1} (s t : Set α) :
                                          theorem Set.offDiag_union {α : Type u_1} {s t : Set α} (h : Disjoint s t) :
                                          theorem Set.offDiag_insert {α : Type u_1} {s : Set α} {a : α} (ha : as) :

                                          Cartesian set-indexed product of sets #

                                          @[simp]
                                          theorem Set.empty_pi {ι : Type u_1} {α : ιType u_2} (s : (i : ι) → Set (α i)) :
                                          theorem Set.subsingleton_univ_pi {ι : Type u_1} {α : ιType u_2} {t : (i : ι) → Set (α i)} (ht : ∀ (i : ι), (t i).Subsingleton) :
                                          @[simp]
                                          theorem Set.pi_univ {ι : Type u_1} {α : ιType u_2} (s : Set ι) :
                                          (s.pi fun (i : ι) => univ) = univ
                                          @[simp]
                                          theorem Set.pi_univ_ite {ι : Type u_1} {α : ιType u_2} (s : Set ι) [DecidablePred fun (x : ι) => x s] (t : (i : ι) → Set (α i)) :
                                          (univ.pi fun (i : ι) => if i s then t i else univ) = s.pi t
                                          theorem Set.pi_mono {ι : Type u_1} {α : ιType u_2} {s : Set ι} {t₁ t₂ : (i : ι) → Set (α i)} (h : is, t₁ i t₂ i) :
                                          s.pi t₁ s.pi t₂
                                          theorem Set.pi_inter_distrib {ι : Type u_1} {α : ιType u_2} {s : Set ι} {t t₁ : (i : ι) → Set (α i)} :
                                          (s.pi fun (i : ι) => t i t₁ i) = s.pi t s.pi t₁
                                          theorem Set.pi_congr {ι : Type u_1} {α : ιType u_2} {s₁ s₂ : Set ι} {t₁ t₂ : (i : ι) → Set (α i)} (h : s₁ = s₂) (h' : is₁, t₁ i = t₂ i) :
                                          s₁.pi t₁ = s₂.pi t₂
                                          theorem Set.pi_eq_empty {ι : Type u_1} {α : ιType u_2} {s : Set ι} {t : (i : ι) → Set (α i)} {i : ι} (hs : i s) (ht : t i = ) :
                                          s.pi t =
                                          theorem Set.univ_pi_eq_empty {ι : Type u_1} {α : ιType u_2} {t : (i : ι) → Set (α i)} {i : ι} (ht : t i = ) :
                                          theorem Set.pi_nonempty_iff {ι : Type u_1} {α : ιType u_2} {s : Set ι} {t : (i : ι) → Set (α i)} :
                                          (s.pi t).Nonempty ∀ (i : ι), ∃ (x : α i), i sx t i
                                          theorem Set.univ_pi_nonempty_iff {ι : Type u_1} {α : ιType u_2} {t : (i : ι) → Set (α i)} :
                                          (univ.pi t).Nonempty ∀ (i : ι), (t i).Nonempty
                                          theorem Set.pi_eq_empty_iff {ι : Type u_1} {α : ιType u_2} {s : Set ι} {t : (i : ι) → Set (α i)} :
                                          s.pi t = ∃ (i : ι), IsEmpty (α i) i s t i =
                                          @[simp]
                                          theorem Set.univ_pi_eq_empty_iff {ι : Type u_1} {α : ιType u_2} {t : (i : ι) → Set (α i)} :
                                          univ.pi t = ∃ (i : ι), t i =
                                          @[simp]
                                          theorem Set.univ_pi_empty {ι : Type u_1} {α : ιType u_2} [h : Nonempty ι] :
                                          (univ.pi fun (x : ι) => ) =
                                          @[simp]
                                          theorem Set.disjoint_univ_pi {ι : Type u_1} {α : ιType u_2} {t₁ t₂ : (i : ι) → Set (α i)} :
                                          Disjoint (univ.pi t₁) (univ.pi t₂) ∃ (i : ι), Disjoint (t₁ i) (t₂ i)
                                          theorem Set.Disjoint.set_pi {ι : Type u_1} {α : ιType u_2} {s : Set ι} {t₁ t₂ : (i : ι) → Set (α i)} {i : ι} (hi : i s) (ht : Disjoint (t₁ i) (t₂ i)) :
                                          Disjoint (s.pi t₁) (s.pi t₂)
                                          theorem Set.uniqueElim_preimage {ι : Type u_1} {α : ιType u_2} [Unique ι] (t : (i : ι) → Set (α i)) :
                                          theorem Set.pi_eq_empty_iff' {ι : Type u_1} {α : ιType u_2} {s : Set ι} {t : (i : ι) → Set (α i)} [∀ (i : ι), Nonempty (α i)] :
                                          s.pi t = is, t i =
                                          @[simp]
                                          theorem Set.disjoint_pi {ι : Type u_1} {α : ιType u_2} {s : Set ι} {t₁ t₂ : (i : ι) → Set (α i)} [∀ (i : ι), Nonempty (α i)] :
                                          Disjoint (s.pi t₁) (s.pi t₂) is, Disjoint (t₁ i) (t₂ i)
                                          @[simp]
                                          theorem Set.insert_pi {ι : Type u_1} {α : ιType u_2} (i : ι) (s : Set ι) (t : (i : ι) → Set (α i)) :
                                          (insert i s).pi t = Function.eval i ⁻¹' t i s.pi t
                                          @[simp]
                                          theorem Set.singleton_pi {ι : Type u_1} {α : ιType u_2} (i : ι) (t : (i : ι) → Set (α i)) :
                                          theorem Set.singleton_pi' {ι : Type u_1} {α : ιType u_2} (i : ι) (t : (i : ι) → Set (α i)) :
                                          {i}.pi t = {x : (i : ι) → α i | x i t i}
                                          theorem Set.univ_pi_singleton {ι : Type u_1} {α : ιType u_2} (f : (i : ι) → α i) :
                                          (univ.pi fun (i : ι) => {f i}) = {f}
                                          theorem Set.preimage_pi {ι : Type u_1} {α : ιType u_2} {β : ιType u_3} (s : Set ι) (t : (i : ι) → Set (β i)) (f : (i : ι) → α iβ i) :
                                          (fun (g : (i : ι) → α i) (i : ι) => f i (g i)) ⁻¹' s.pi t = s.pi fun (i : ι) => f i ⁻¹' t i
                                          theorem Set.pi_if {ι : Type u_1} {α : ιType u_2} {p : ιProp} [h : DecidablePred p] (s : Set ι) (t₁ t₂ : (i : ι) → Set (α i)) :
                                          (s.pi fun (i : ι) => if p i then t₁ i else t₂ i) = {i : ι | i s p i}.pi t₁ {i : ι | i s ¬p i}.pi t₂
                                          theorem Set.union_pi {ι : Type u_1} {α : ιType u_2} {s₁ s₂ : Set ι} {t : (i : ι) → Set (α i)} :
                                          (s₁ s₂).pi t = s₁.pi t s₂.pi t
                                          theorem Set.union_pi_inter {ι : Type u_1} {α : ιType u_2} {s₁ s₂ : Set ι} {t₁ t₂ : (i : ι) → Set (α i)} (ht₁ : is₁, t₁ i = univ) (ht₂ : is₂, t₂ i = univ) :
                                          ((s₁ s₂).pi fun (i : ι) => t₁ i t₂ i) = s₁.pi t₁ s₂.pi t₂
                                          @[simp]
                                          theorem Set.pi_inter_compl {ι : Type u_1} {α : ιType u_2} {t : (i : ι) → Set (α i)} (s : Set ι) :
                                          s.pi t s.pi t = univ.pi t
                                          theorem Set.pi_update_of_notMem {ι : Type u_1} {α : ιType u_2} {β : ιType u_3} {s : Set ι} {i : ι} [DecidableEq ι] (hi : is) (f : (j : ι) → α j) (a : α i) (t : (j : ι) → α jSet (β j)) :
                                          (s.pi fun (j : ι) => t j (Function.update f i a j)) = s.pi fun (j : ι) => t j (f j)
                                          @[deprecated Set.pi_update_of_notMem (since := "2025-05-23")]
                                          theorem Set.pi_update_of_not_mem {ι : Type u_1} {α : ιType u_2} {β : ιType u_3} {s : Set ι} {i : ι} [DecidableEq ι] (hi : is) (f : (j : ι) → α j) (a : α i) (t : (j : ι) → α jSet (β j)) :
                                          (s.pi fun (j : ι) => t j (Function.update f i a j)) = s.pi fun (j : ι) => t j (f j)

                                          Alias of Set.pi_update_of_notMem.

                                          theorem Set.pi_update_of_mem {ι : Type u_1} {α : ιType u_2} {β : ιType u_3} {s : Set ι} {i : ι} [DecidableEq ι] (hi : i s) (f : (j : ι) → α j) (a : α i) (t : (j : ι) → α jSet (β j)) :
                                          (s.pi fun (j : ι) => t j (Function.update f i a j)) = {x : (i : ι) → β i | x i t i a} (s \ {i}).pi fun (j : ι) => t j (f j)
                                          theorem Set.univ_pi_update {ι : Type u_1} {α : ιType u_2} [DecidableEq ι] {β : ιType u_4} (i : ι) (f : (j : ι) → α j) (a : α i) (t : (j : ι) → α jSet (β j)) :
                                          (univ.pi fun (j : ι) => t j (Function.update f i a j)) = {x : (i : ι) → β i | x i t i a} {i}.pi fun (j : ι) => t j (f j)
                                          theorem Set.univ_pi_update_univ {ι : Type u_1} {α : ιType u_2} [DecidableEq ι] (i : ι) (s : Set (α i)) :
                                          univ.pi (Function.update (fun (j : ι) => univ) i s) = Function.eval i ⁻¹' s
                                          theorem Set.eval_image_pi_subset {ι : Type u_1} {α : ιType u_2} {s : Set ι} {t : (i : ι) → Set (α i)} {i : ι} (hs : i s) :
                                          theorem Set.eval_image_univ_pi_subset {ι : Type u_1} {α : ιType u_2} {t : (i : ι) → Set (α i)} {i : ι} :
                                          theorem Set.subset_eval_image_pi {ι : Type u_1} {α : ιType u_2} {s : Set ι} {t : (i : ι) → Set (α i)} (ht : (s.pi t).Nonempty) (i : ι) :
                                          theorem Set.eval_image_pi {ι : Type u_1} {α : ιType u_2} {s : Set ι} {t : (i : ι) → Set (α i)} {i : ι} (hs : i s) (ht : (s.pi t).Nonempty) :
                                          Function.eval i '' s.pi t = t i
                                          theorem Set.eval_image_pi_of_notMem {ι : Type u_1} {α : ιType u_2} {s : Set ι} {t : (i : ι) → Set (α i)} {i : ι} [Decidable (s.pi t).Nonempty] (hi : is) :
                                          @[deprecated Set.eval_image_pi_of_notMem (since := "2025-05-23")]
                                          theorem Set.eval_image_pi_of_not_mem {ι : Type u_1} {α : ιType u_2} {s : Set ι} {t : (i : ι) → Set (α i)} {i : ι} [Decidable (s.pi t).Nonempty] (hi : is) :

                                          Alias of Set.eval_image_pi_of_notMem.

                                          @[simp]
                                          theorem Set.eval_image_univ_pi {ι : Type u_1} {α : ιType u_2} {t : (i : ι) → Set (α i)} {i : ι} (ht : (univ.pi t).Nonempty) :
                                          (fun (f : (i : ι) → α i) => f i) '' univ.pi t = t i
                                          theorem Set.piMap_mapsTo_pi {ι : Type u_1} {α : ιType u_2} {β : ιType u_3} {I : Set ι} {f : (i : ι) → α iβ i} {s : (i : ι) → Set (α i)} {t : (i : ι) → Set (β i)} (h : iI, MapsTo (f i) (s i) (t i)) :
                                          MapsTo (Pi.map f) (I.pi s) (I.pi t)
                                          theorem Set.piMap_image_pi_subset {ι : Type u_1} {α : ιType u_2} {β : ιType u_3} {s : Set ι} {f : (i : ι) → α iβ i} (t : (i : ι) → Set (α i)) :
                                          Pi.map f '' s.pi t s.pi fun (i : ι) => f i '' t i
                                          theorem Set.piMap_image_pi {ι : Type u_1} {α : ιType u_2} {β : ιType u_3} {s : Set ι} {f : (i : ι) → α iβ i} (hf : is, Function.Surjective (f i)) (t : (i : ι) → Set (α i)) :
                                          Pi.map f '' s.pi t = s.pi fun (i : ι) => f i '' t i
                                          theorem Set.piMap_image_univ_pi {ι : Type u_1} {α : ιType u_2} {β : ιType u_3} (f : (i : ι) → α iβ i) (t : (i : ι) → Set (α i)) :
                                          Pi.map f '' univ.pi t = univ.pi fun (i : ι) => f i '' t i
                                          @[simp]
                                          theorem Set.range_piMap {ι : Type u_1} {α : ιType u_2} {β : ιType u_3} (f : (i : ι) → α iβ i) :
                                          range (Pi.map f) = univ.pi fun (i : ι) => range (f i)
                                          theorem Set.pi_subset_pi_iff {ι : Type u_1} {α : ιType u_2} {s : Set ι} {t₁ t₂ : (i : ι) → Set (α i)} :
                                          s.pi t₁ s.pi t₂ (∀ is, t₁ i t₂ i) s.pi t₁ =
                                          theorem Set.univ_pi_subset_univ_pi_iff {ι : Type u_1} {α : ιType u_2} {t₁ t₂ : (i : ι) → Set (α i)} :
                                          univ.pi t₁ univ.pi t₂ (∀ (i : ι), t₁ i t₂ i) ∃ (i : ι), t₁ i =
                                          theorem Set.eval_preimage {ι : Type u_1} {α : ιType u_2} {i : ι} [DecidableEq ι] {s : Set (α i)} :
                                          Function.eval i ⁻¹' s = univ.pi (Function.update (fun (x : ι) => univ) i s)
                                          theorem Set.eval_preimage' {ι : Type u_1} {α : ιType u_2} {i : ι} [DecidableEq ι] {s : Set (α i)} :
                                          Function.eval i ⁻¹' s = {i}.pi (Function.update (fun (x : ι) => univ) i s)
                                          theorem Set.update_preimage_pi {ι : Type u_1} {α : ιType u_2} {s : Set ι} {t : (i : ι) → Set (α i)} {i : ι} [DecidableEq ι] {f : (i : ι) → α i} (hi : i s) (hf : js, j if j t j) :
                                          theorem Set.update_image {ι : Type u_1} {β : ιType u_3} [DecidableEq ι] (x : (i : ι) → β i) (i : ι) (s : Set (β i)) :
                                          Function.update x i '' s = univ.pi (Function.update (fun (j : ι) => {x j}) i s)
                                          theorem Set.update_preimage_univ_pi {ι : Type u_1} {α : ιType u_2} {t : (i : ι) → Set (α i)} {i : ι} [DecidableEq ι] {f : (i : ι) → α i} (hf : ∀ (j : ι), j if j t j) :
                                          theorem Set.subset_pi_eval_image {ι : Type u_1} {α : ιType u_2} (s : Set ι) (u : Set ((i : ι) → α i)) :
                                          u s.pi fun (i : ι) => Function.eval i '' u
                                          theorem Set.univ_pi_ite {ι : Type u_1} {α : ιType u_2} (s : Set ι) [DecidablePred fun (x : ι) => x s] (t : (i : ι) → Set (α i)) :
                                          (univ.pi fun (i : ι) => if i s then t i else univ) = s.pi t
                                          theorem Equiv.piCongrLeft_symm_preimage_pi {ι : Type u_1} {ι' : Type u_2} {α : ιType u_3} (f : ι' ι) (s : Set ι') (t : (i : ι) → Set (α i)) :
                                          ((piCongrLeft α f).symm ⁻¹' s.pi fun (i' : ι') => t (f i')) = (f '' s).pi t
                                          theorem Equiv.piCongrLeft_symm_preimage_univ_pi {ι : Type u_1} {ι' : Type u_2} {α : ιType u_3} (f : ι' ι) (t : (i : ι) → Set (α i)) :
                                          ((piCongrLeft α f).symm ⁻¹' Set.univ.pi fun (i' : ι') => t (f i')) = Set.univ.pi t
                                          theorem Equiv.piCongrLeft_preimage_pi {ι : Type u_1} {ι' : Type u_2} {α : ιType u_3} (f : ι' ι) (s : Set ι') (t : (i : ι) → Set (α i)) :
                                          (piCongrLeft α f) ⁻¹' (f '' s).pi t = s.pi fun (i : ι') => t (f i)
                                          theorem Equiv.piCongrLeft_preimage_univ_pi {ι : Type u_1} {ι' : Type u_2} {α : ιType u_3} (f : ι' ι) (t : (i : ι) → Set (α i)) :
                                          (piCongrLeft α f) ⁻¹' Set.univ.pi t = Set.univ.pi fun (i : ι') => t (f i)
                                          theorem Equiv.sumPiEquivProdPi_symm_preimage_univ_pi {ι : Type u_1} {ι' : Type u_2} (π : ι ι'Type u_4) (t : (i : ι ι') → Set (π i)) :
                                          (sumPiEquivProdPi π).symm ⁻¹' Set.univ.pi t = (Set.univ.pi fun (i : ι) => t (Sum.inl i)) ×ˢ Set.univ.pi fun (i : ι') => t (Sum.inr i)
                                          @[simp]
                                          theorem Set.mem_graphOn {α : Type u_1} {β : Type u_2} {s : Set α} {f : αβ} {x : α × β} :
                                          x graphOn f s x.1 s f x.1 = x.2
                                          @[simp]
                                          theorem Set.graphOn_empty {α : Type u_1} {β : Type u_2} (f : αβ) :
                                          @[simp]
                                          theorem Set.graphOn_eq_empty {α : Type u_1} {β : Type u_2} {s : Set α} {f : αβ} :
                                          @[simp]
                                          theorem Set.graphOn_nonempty {α : Type u_1} {β : Type u_2} {s : Set α} {f : αβ} :
                                          theorem Set.Nonempty.graphOn {α : Type u_1} {β : Type u_2} {s : Set α} {f : αβ} :

                                          Alias of the reverse direction of Set.graphOn_nonempty.

                                          @[simp]
                                          theorem Set.graphOn_union {α : Type u_1} {β : Type u_2} (f : αβ) (s t : Set α) :
                                          graphOn f (s t) = graphOn f s graphOn f t
                                          @[simp]
                                          theorem Set.graphOn_singleton {α : Type u_1} {β : Type u_2} (f : αβ) (x : α) :
                                          graphOn f {x} = {(x, f x)}
                                          @[simp]
                                          theorem Set.graphOn_insert {α : Type u_1} {β : Type u_2} (f : αβ) (x : α) (s : Set α) :
                                          graphOn f (insert x s) = insert (x, f x) (graphOn f s)
                                          @[simp]
                                          theorem Set.image_fst_graphOn {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set α) :
                                          @[simp]
                                          theorem Set.image_snd_graphOn {α : Type u_1} {β : Type u_2} {s : Set α} (f : αβ) :
                                          theorem Set.fst_injOn_graph {α : Type u_1} {β : Type u_2} {s : Set α} {f : αβ} :
                                          theorem Set.graphOn_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (s : Set α) (f : αβ) (g : βγ) :
                                          graphOn (g f) s = (fun (x : α × β) => (x.1, g x.2)) '' graphOn f s
                                          theorem Set.graphOn_univ_eq_range {α : Type u_1} {β : Type u_2} {f : αβ} :
                                          graphOn f univ = range fun (x : α) => (x, f x)
                                          @[simp]
                                          theorem Set.graphOn_inj {α : Type u_1} {β : Type u_2} {s : Set α} {f g : αβ} :
                                          graphOn f s = graphOn g s EqOn f g s
                                          theorem Set.graphOn_prod_graphOn {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (s : Set α) (t : Set β) (f : αγ) (g : βδ) :
                                          graphOn f s ×ˢ graphOn g t = (Equiv.prodProdProdComm α γ β δ) ⁻¹' graphOn (Prod.map f g) (s ×ˢ t)
                                          theorem Set.graphOn_prod_prodMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (s : Set α) (t : Set β) (f : αγ) (g : βδ) :
                                          graphOn (Prod.map f g) (s ×ˢ t) = (Equiv.prodProdProdComm α β γ δ) ⁻¹' graphOn f s ×ˢ graphOn g t

                                          Vertical line test #

                                          theorem Set.exists_range_eq_graphOn_univ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : αβ × γ} (hf₁ : Function.Surjective (Prod.fst f)) (hf : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1(f g₁).2 = (f g₂).2) :
                                          ∃ (f' : βγ), range f = graphOn f' univ

                                          Vertical line test for functions.

                                          Let f : α → β × γ be a function to a product. Assume that f is surjective on the first factor and that the image of f intersects every "vertical line" {(b, c) | c : γ} at most once. Then the image of f is the graph of some monoid homomorphism f' : β → γ.

                                          theorem Set.exists_equiv_range_eq_graphOn_univ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : αβ × γ} (hf₁ : Function.Surjective (Prod.fst f)) (hf₂ : Function.Surjective (Prod.snd f)) (hf : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 (f g₁).2 = (f g₂).2) :
                                          ∃ (e : β γ), range f = graphOn (⇑e) univ

                                          Line test for equivalences.

                                          Let f : α → β × γ be a homomorphism to a product of monoids. Assume that f is surjective on both factors and that the image of f intersects every "vertical line" {(b, c) | c : γ} and every "horizontal line" {(b, c) | b : β} at most once. Then the image of f is the graph of some equivalence f' : β ≃ γ.

                                          theorem Set.exists_eq_mgraphOn_univ {β : Type u_2} {γ : Type u_3} {s : Set (β × γ)} (hs₁ : Function.Bijective (Prod.fst Subtype.val)) :
                                          ∃ (f : βγ), s = graphOn f univ

                                          Vertical line test for functions.

                                          Let s : Set (β × γ) be a set in a product. Assume that s maps bijectively to the first factor. Then s is the graph of some function f : β → γ.