data.set.prod

# Sets in product and pi types #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines the product of sets in α × β and in Π i, α i along with the diagonal of a type.

## Main declarations #

• set.prod: Binary product of sets. For s : set α, t : set β, we have s.prod t : set (α × β).
• set.diagonal: Diagonal of a type. set.diagonal α = {(x, x) | x : α}.
• set.off_diag: Off-diagonal. s ×ˢ s without the diagonal.
• set.pi: Arbitrary product of sets.

### Cartesian binary product of sets #

def set.prod {α : Type u_1} {β : Type u_2} (s : set α) (t : set β) :
set × β)

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

Equations
Instances for ↥set.prod
theorem set.prod_eq {α : Type u_1} {β : Type u_2} (s : set α) (t : set β) :
s ×ˢ t =
theorem set.mem_prod_eq {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} {p : α × β} :
p s ×ˢ t = (p.fst s p.snd t)
@[simp]
theorem set.mem_prod {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} {p : α × β} :
p s ×ˢ t p.fst s p.snd t
@[simp]
theorem set.prod_mk_mem_set_prod_eq {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} {a : α} {b : β} :
(a, b) s ×ˢ t = (a s b t)
theorem set.mk_mem_prod {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} {a : α} {b : β} (ha : a s) (hb : b t) :
(a, b) s ×ˢ t
@[protected, instance]
def set.decidable_mem_prod {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} [hs : decidable_pred (λ (_x : α), _x s)] [ht : decidable_pred (λ (_x : β), _x t)] :
decidable_pred (λ (_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 (x : α), x s (y : β), y t (x, y) P
theorem set.forall_prod_set {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} {p : α × β Prop} :
( (x : α × β), x s ×ˢ t p x) (x : α), x s (y : β), y t p (x, y)
theorem set.exists_prod_set {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} {p : α × β Prop} :
( (x : α × β) (H : x s ×ˢ t), p x) (x : α) (H : x s) (y : β) (H : y t), 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.singleton_prod {α : Type u_1} {β : Type u_2} {t : set β} {a : α} :
{a} ×ˢ t = '' t
@[simp]
theorem set.prod_singleton {α : Type u_1} {β : Type u_2} {s : set α} {b : β} :
s ×ˢ {b} = (λ (a : α), (a, b)) '' s
theorem set.singleton_prod_singleton {α : Type u_1} {β : Type u_2} {a : α} {b : β} :
{a} ×ˢ {b} = {(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.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.insert_prod {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} {a : α} :
×ˢ t = '' t s ×ˢ t
theorem set.prod_insert {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} {b : β} :
s ×ˢ = (λ (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) = (λ (p : γ × δ), (f p.fst, g p.snd)) ⁻¹' s ×ˢ t
theorem set.prod_preimage_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : set α} {t : set β} {f : γ α} :
(f ⁻¹' s) ×ˢ t = (λ (p : γ × β), (f p.fst, p.snd)) ⁻¹' s ×ˢ t
theorem set.prod_preimage_right {α : Type u_1} {β : Type u_2} {δ : Type u_4} {s : set α} {t : set β} {g : δ β} :
s ×ˢ (g ⁻¹' t) = (λ (p : α × δ), (p.fst, g p.snd)) ⁻¹' 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 δ) :
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 : γ β) :
(λ (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) :
(λ (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) :
⁻¹' s ×ˢ t = t
@[simp]
theorem set.mk_preimage_prod_left_eq_empty {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} {b : β} (hb : b t) :
(λ (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 : a s) :
theorem set.mk_preimage_prod_left_eq_if {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} {b : β} [decidable_pred (λ (_x : β), _x t)] :
(λ (a : α), (a, b)) ⁻¹' s ×ˢ t = ite (b t) s
theorem set.mk_preimage_prod_right_eq_if {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} {a : α} [decidable_pred (λ (_x : α), _x s)] :
⁻¹' s ×ˢ t = ite (a s) t
theorem set.mk_preimage_prod_left_fn_eq_if {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : set α} {t : set β} {b : β} [decidable_pred (λ (_x : β), _x t)] (f : γ α) :
(λ (a : γ), (f a, b)) ⁻¹' s ×ˢ t = ite (b t) (f ⁻¹' s)
theorem set.mk_preimage_prod_right_fn_eq_if {α : Type u_1} {β : Type u_2} {δ : Type u_4} {s : set α} {t : set β} {a : α} [decidable_pred (λ (_x : α), _x s)] (g : δ β) :
(λ (b : δ), (a, g b)) ⁻¹' s ×ˢ t = ite (a s) (g ⁻¹' t)
@[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.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) = (λ (p : α × β), (m₁ p.fst, m₂ p.snd)) '' s ×ˢ t
theorem set.prod_range_range_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {m₁ : α γ} {m₂ : β δ} :
×ˢ = set.range (λ (p : α × β), (m₁ p.fst, m₂ p.snd))
@[simp]
theorem set.range_prod_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {m₁ : α γ} {m₂ : β δ} :
set.range (prod.map m₁ m₂) = ×ˢ
theorem set.prod_range_univ_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m₁ : α γ} :
= set.range (λ (p : α × β), (m₁ p.fst, p.snd))
theorem set.prod_univ_range_eq {α : Type u_1} {β : Type u_2} {δ : Type u_4} {m₂ : β δ} :
= set.range (λ (p : α × β), (p.fst, m₂ p.snd))
theorem set.range_pair_subset {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α β) (g : α γ) :
set.range (λ (x : α), (f x, g x))
theorem set.nonempty.prod {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} :
theorem set.nonempty.fst {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} :
theorem set.nonempty.snd {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} :
theorem set.prod_nonempty_iff {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} :
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 s b t f (a, b) W
theorem set.image_prod_mk_subset_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α β} {g : α γ} {s : set α} :
(λ (x : α), (f x, g x)) '' s (f '' s) ×ˢ (g '' s)
theorem set.image_prod_mk_subset_prod_left {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} {b : β} (hb : b t) :
(λ (a : α), (a, b)) '' s s ×ˢ t
theorem set.image_prod_mk_subset_prod_right {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} {a : α} (ha : a s) :
'' t s ×ˢ t
theorem set.prod_subset_preimage_fst {α : Type u_1} {β : Type u_2} (s : set α) (t : set β) :
s ×ˢ t
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.prod_subset_preimage_snd {α : Type u_1} {β : Type u_2} (s : set α) (t : set β) :
s ×ˢ t
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.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 monotone.set_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} [preorder α] {f : α set β} {g : α set γ} (hf : monotone f) (hg : monotone g) :
monotone (λ (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 (λ (x : α), f x ×ˢ g x)
theorem monotone_on.set_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : set α} [preorder α] {f : α set β} {g : α set γ} (hf : s) (hg : s) :
monotone_on (λ (x : α), f x ×ˢ g x) s
theorem antitone_on.set_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : set α} [preorder α] {f : α set β} {g : α set γ} (hf : s) (hg : s) :
antitone_on (λ (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 λ x, (x, x).

def set.diagonal (α : Type u_1) :
set × α)

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

Equations
theorem set.mem_diagonal {α : Type u_1} (x : α) :
(x, x)
@[simp]
theorem set.mem_diagonal_iff {α : Type u_1} {x : α × α} :
x.fst = x.snd
@[protected, instance]
def set.decidable_mem_diagonal {α : Type u_1} [h : decidable_eq α] (x : α × α) :
Equations
theorem set.preimage_coe_coe_diagonal {α : Type u_1} (s : set α) :
@[simp]
theorem set.range_diag {α : Type u_1} :
set.range (λ (x : α), (x, x)) =
theorem set.diagonal_subset_iff {α : Type u_1} {s : set × α)} :
(x : α), (x, x) s
@[simp]
theorem set.prod_subset_compl_diagonal_iff_disjoint {α : Type u_1} {s t : set α} :
@[simp]
theorem set.diag_preimage_prod {α : Type u_1} (s t : set α) :
(λ (x : α), (x, x)) ⁻¹' s ×ˢ t = s t
theorem set.diag_preimage_prod_self {α : Type u_1} (s : set α) :
(λ (x : α), (x, x)) ⁻¹' s ×ˢ s = s
theorem set.diag_image {α : Type u_1} (s : set α) :
(λ (x : α), (x, x)) '' s = s ×ˢ s
def set.off_diag {α : Type u_1} (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 ↥set.off_diag
@[simp]
theorem set.mem_off_diag {α : Type u_1} {s : set α} {x : α × α} :
theorem set.off_diag_mono {α : Type u_1} :
@[simp]
theorem set.off_diag_nonempty {α : Type u_1} {s : set α} :
@[simp]
theorem set.off_diag_eq_empty {α : Type u_1} {s : set α} :
theorem set.nontrivial.off_diag_nonempty {α : Type u_1} {s : set α} :

Alias of the reverse direction of set.off_diag_nonempty.

theorem set.subsingleton.off_diag_eq_empty {α : Type u_1} {s : set α} :

Alias of the reverse direction of set.off_diag_nonempty.

theorem set.off_diag_subset_prod {α : Type u_1} (s : set α) :
theorem set.off_diag_eq_sep_prod {α : Type u_1} (s : set α) :
s.off_diag = {x ∈ s ×ˢ s | x.fst x.snd}
@[simp]
theorem set.off_diag_empty {α : Type u_1} :
@[simp]
theorem set.off_diag_singleton {α : Type u_1} (a : α) :
@[simp]
theorem set.off_diag_univ {α : Type u_1} :
@[simp]
theorem set.prod_sdiff_diagonal {α : Type u_1} (s : set α) :
@[simp]
theorem set.disjoint_diagonal_off_diag {α : Type u_1} (s : set α) :
theorem set.off_diag_inter {α : Type u_1} (s t : set α) :
(s t).off_diag =
theorem set.off_diag_union {α : Type u_1} {s t : set α} (h : t) :
(s t).off_diag = s ×ˢ t t ×ˢ s
theorem set.off_diag_insert {α : Type u_1} {s : set α} {a : α} (ha : a s) :
s).off_diag = s.off_diag {a} ×ˢ s s ×ˢ {a}

### Cartesian set-indexed product of sets #

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
Instances for set.pi
@[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 s f i t i
@[simp]
theorem set.mem_univ_pi {ι : Type u_1} {α : ι Type u_2} {t : Π (i : ι), set (α i)} {f : Π (i : ι), α i} :
f (i : ι), f i t i
@[simp]
theorem set.empty_pi {ι : Type u_1} {α : ι Type u_2} (s : Π (i : ι), set (α i)) :
@[simp]
theorem set.pi_univ {ι : Type u_1} {α : ι Type u_2} (s : set ι) :
s.pi (λ (i : ι), set.univ) = set.univ
theorem set.pi_mono {ι : Type u_1} {α : ι Type u_2} {s : set ι} {t₁ t₂ : Π (i : ι), set (α i)} (h : (i : ι), i s 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 (λ (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' : (i : ι), i s₁ 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 s x t i
theorem set.univ_pi_nonempty_iff {ι : Type u_1} {α : ι Type u_2} {t : Π (i : ι), set (α i)} :
(set.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 : ι), is_empty (α i) i s t i =
@[simp]
theorem set.univ_pi_eq_empty_iff {ι : Type u_1} {α : ι Type u_2} {t : Π (i : ι), set (α i)} :
= (i : ι), t i =
@[simp]
theorem set.univ_pi_empty {ι : Type u_1} {α : ι Type u_2} [h : nonempty ι] :
set.univ.pi (λ (i : ι), ) =
@[simp]
theorem set.disjoint_univ_pi {ι : Type u_1} {α : ι Type u_2} {t₁ t₂ : Π (i : ι), set (α i)} :
disjoint (set.univ.pi t₁) (set.univ.pi t₂) (i : ι), disjoint (t₁ i) (t₂ i)
@[simp]
theorem set.range_dcomp {ι : Type u_1} {α : ι Type u_2} {β : ι Type u_3} (f : Π (i : ι), α i β i) :
set.range (λ (g : Π (i : ι), α i) (i : ι), f i (g i)) = set.univ.pi (λ (i : ι), set.range (f i))
@[simp]
theorem set.insert_pi {ι : Type u_1} {α : ι Type u_2} (i : ι) (s : set ι) (t : Π (i : ι), set (α i)) :
s).pi t = ⁻¹' t i s.pi t
@[simp]
theorem set.singleton_pi {ι : Type u_1} {α : ι Type u_2} (i : ι) (t : Π (i : ι), set (α i)) :
{i}.pi t = ⁻¹' t 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) :
set.univ.pi (λ (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) :
(λ (g : Π (i : ι), α i) (i : ι), f i (g i)) ⁻¹' s.pi t = s.pi (λ (i : ι), f i ⁻¹' t i)
theorem set.pi_if {ι : Type u_1} {α : ι Type u_2} {p : ι Prop} [h : decidable_pred p] (s : set ι) (t₁ t₂ : Π (i : ι), set (α i)) :
s.pi (λ (i : ι), ite (p i) (t₁ i) (t₂ i)) = {i ∈ s | p i}.pi t₁ {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
@[simp]
theorem set.pi_inter_compl {ι : Type u_1} {α : ι Type u_2} {t : Π (i : ι), set (α i)} (s : set ι) :
s.pi t s.pi t =
theorem set.pi_update_of_not_mem {ι : Type u_1} {α : ι Type u_2} {β : ι Type u_3} {s : set ι} {i : ι} [decidable_eq ι] (hi : i s) (f : Π (j : ι), α j) (a : α i) (t : Π (j : ι), α j set (β j)) :
s.pi (λ (j : ι), t j i a j)) = s.pi (λ (j : ι), t j (f j))
theorem set.pi_update_of_mem {ι : Type u_1} {α : ι Type u_2} {β : ι Type u_3} {s : set ι} {i : ι} [decidable_eq ι] (hi : i s) (f : Π (j : ι), α j) (a : α i) (t : Π (j : ι), α j set (β j)) :
s.pi (λ (j : ι), t j i a j)) = {x : Π (i : ι), β i | x i t i a} (s \ {i}).pi (λ (j : ι), t j (f j))
theorem set.univ_pi_update {ι : Type u_1} {α : ι Type u_2} [decidable_eq ι] {β : ι Type u_3} (i : ι) (f : Π (j : ι), α j) (a : α i) (t : Π (j : ι), α j set (β j)) :
set.univ.pi (λ (j : ι), t j i a j)) = {x : Π (i : ι), β i | x i t i a} {i}.pi (λ (j : ι), t j (f j))
theorem set.univ_pi_update_univ {ι : Type u_1} {α : ι Type u_2} [decidable_eq ι] (i : ι) (s : set (α i)) :
set.univ.pi (function.update (λ (j : ι), set.univ) i s) =
theorem set.eval_image_pi_subset {ι : Type u_1} {α : ι Type u_2} {s : set ι} {t : Π (i : ι), set (α i)} {i : ι} (hs : i s) :
'' s.pi t t i
theorem set.eval_image_univ_pi_subset {ι : Type u_1} {α : ι Type u_2} {t : Π (i : ι), set (α i)} {i : ι} :
t 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 : ι) :
t i '' s.pi t
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) :
'' s.pi t = t i
@[simp]
theorem set.eval_image_univ_pi {ι : Type u_1} {α : ι Type u_2} {t : Π (i : ι), set (α i)} {i : ι} (ht : (set.univ.pi t).nonempty) :
(λ (f : Π (i : ι), α i), f i) '' = t 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₂ ( (i : ι), i s 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)} :
set.univ.pi t₁ set.univ.pi t₂ ( (i : ι), t₁ i t₂ i) (i : ι), t₁ i =
theorem set.eval_preimage {ι : Type u_1} {α : ι Type u_2} {i : ι} [decidable_eq ι] {s : set (α i)} :
= set.univ.pi (function.update (λ (i : ι), set.univ) i s)
theorem set.eval_preimage' {ι : Type u_1} {α : ι Type u_2} {i : ι} [decidable_eq ι] {s : set (α i)} :
= {i}.pi (function.update (λ (i : ι), set.univ) i s)
theorem set.update_preimage_pi {ι : Type u_1} {α : ι Type u_2} {s : set ι} {t : Π (i : ι), set (α i)} {i : ι} [decidable_eq ι] {f : Π (i : ι), α i} (hi : i s) (hf : (j : ι), j s j i f j t j) :
⁻¹' s.pi t = t i
theorem set.update_preimage_univ_pi {ι : Type u_1} {α : ι Type u_2} {t : Π (i : ι), set (α i)} {i : ι} [decidable_eq ι] {f : Π (i : ι), α i} (hf : (j : ι), j i f j t j) :
⁻¹' = t i
theorem set.subset_pi_eval_image {ι : Type u_1} {α : ι Type u_2} (s : set ι) (u : set (Π (i : ι), α i)) :
u s.pi (λ (i : ι), '' u)
theorem set.univ_pi_ite {ι : Type u_1} {α : ι Type u_2} (s : set ι) [decidable_pred (λ (_x : ι), _x s)] (t : Π (i : ι), set (α i)) :
set.univ.pi (λ (i : ι), ite (i s) (t i) set.univ) = s.pi t