Documentation

Mathlib.Data.Set.Prod

Sets in product and pi types #

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

Main declarations #

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∈ s and b ∈ t∈ t.

Equations

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

Equations
theorem Set.prod_eq {α : Type u_1} {β : Type u_2} (s : Set α) (t : Set β) :
s ×ˢ t = Prod.fst ⁻¹' s Prod.snd ⁻¹' 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
theorem Set.prod_mk_mem_set_prod_eq {α : Type u_2} {β : Type u_1} {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
noncomputable instance Set.decidableMemProd {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} [inst : DecidablePred fun x => x s] [inst : DecidablePred fun x => x t] :
DecidablePred fun x => x s ×ˢ t
Equations
theorem Set.prod_mono {α : Type u_1} {β : Type u_2} {s₁ : Set α} {s₂ : Set α} {t₁ : Set β} {t₂ : Set β} (hs : s₁ s₂) (ht : t₁ t₂) :
s₁ ×ˢ t₁ s₂ ×ˢ t₂
theorem Set.prod_mono_left {α : Type u_1} {β : Type u_2} {s₁ : Set α} {s₂ : Set α} {t : Set β} (hs : s₁ s₂) :
s₁ ×ˢ t s₂ ×ˢ t
theorem Set.prod_mono_right {α : Type u_2} {β : Type u_1} {s : Set α} {t₁ : Set β} {t₂ : Set β} (ht : t₁ t₂) :
s ×ˢ t₁ s ×ˢ t₂
@[simp]
theorem Set.prod_self_subset_prod_self {α : Type u_1} {s₁ : Set α} {s₂ : Set α} :
s₁ ×ˢ s₁ s₂ ×ˢ s₂ s₁ s₂
@[simp]
theorem Set.prod_self_ssubset_prod_self {α : Type u_1} {s₁ : Set α} {s₂ : Set α} :
s₁ ×ˢ s₁ s₂ ×ˢ s₂ s₁ s₂
theorem Set.prod_subset_iff {α : Type u_2} {β : Type u_1} {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 ×ˢ tp x) (x : α) → x s(y : β) → y tp (x, y)
theorem Set.exists_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)
@[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} :
Set.univ ×ˢ Set.univ = Set.univ
theorem Set.univ_prod {α : Type u_2} {β : Type u_1} {t : Set β} :
Set.univ ×ˢ t = Prod.snd ⁻¹' t
theorem Set.prod_univ {α : Type u_1} {β : Type u_2} {s : Set α} :
s ×ˢ Set.univ = Prod.fst ⁻¹' s
@[simp]
theorem Set.singleton_prod {α : Type u_1} {β : Type u_2} {t : Set β} {a : α} :
{a} ×ˢ t = Prod.mk a '' t
@[simp]
theorem Set.prod_singleton {α : Type u_1} {β : Type u_2} {s : Set α} {b : β} :
s ×ˢ {b} = (fun 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₁ : Set α} {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₁ : Set β} {t₂ : Set β} :
s ×ˢ (t₁ t₂) = s ×ˢ t₁ s ×ˢ t₂
theorem Set.inter_prod {α : Type u_1} {β : Type u_2} {s₁ : Set α} {s₂ : Set α} {t : Set β} :
(s₁ s₂) ×ˢ t = s₁ ×ˢ t s₂ ×ˢ t
theorem Set.prod_inter {α : Type u_1} {β : Type u_2} {s : Set α} {t₁ : Set β} {t₂ : Set β} :
s ×ˢ (t₁ t₂) = s ×ˢ t₁ s ×ˢ t₂
theorem Set.prod_inter_prod {α : Type u_1} {β : Type u_2} {s₁ : Set α} {s₂ : Set α} {t₁ : Set β} {t₂ : Set β} :
s₁ ×ˢ t₁ s₂ ×ˢ t₂ = (s₁ s₂) ×ˢ (t₁ t₂)
theorem Set.disjoint_prod {α : Type u_2} {β : Type u_1} {s₁ : Set α} {s₂ : Set α} {t₁ : Set β} {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 : α} :
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_3} {β : Type u_4} {γ : Type u_1} {δ : Type u_2} {s : Set α} {t : Set β} {f : γα} {g : δβ} :
(f ⁻¹' s) ×ˢ (g ⁻¹' t) = (fun p => (f p.fst, g p.snd)) ⁻¹' s ×ˢ t
theorem Set.prod_preimage_left {α : Type u_3} {β : Type u_1} {γ : Type u_2} {s : Set α} {t : Set β} {f : γα} :
(f ⁻¹' s) ×ˢ t = (fun p => (f p.fst, p.snd)) ⁻¹' s ×ˢ t
theorem Set.prod_preimage_right {α : Type u_1} {β : Type u_3} {δ : Type u_2} {s : Set α} {t : Set β} {g : δβ} :
s ×ˢ (g ⁻¹' t) = (fun p => (p.fst, g p.snd)) ⁻¹' s ×ˢ t
theorem Set.preimage_prod_map_prod {α : Type u_3} {β : Type u_1} {γ : Type u_4} {δ : Type u_2} (f : αβ) (g : γδ) (s : Set β) (t : Set δ) :
Prod.map f g ⁻¹' s ×ˢ t = (f ⁻¹' s) ×ˢ (g ⁻¹' t)
theorem Set.mk_preimage_prod {α : Type u_3} {β : Type u_2} {γ : Type u_1} {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_2} {β : Type u_1} {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_2} {β : Type u_1} {s : Set α} {t : Set β} {b : β} (hb : ¬b t) :
(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 : ¬a s) :
theorem Set.mk_preimage_prod_left_eq_if {α : Type u_2} {β : Type u_1} {s : Set α} {t : Set β} {b : β} [inst : 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 : α} [inst : DecidablePred fun x => x s] :
Prod.mk a ⁻¹' s ×ˢ t = if a s then t else
theorem Set.mk_preimage_prod_left_fn_eq_if {α : Type u_3} {β : Type u_1} {γ : Type u_2} {s : Set α} {t : Set β} {b : β} [inst : 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_3} {δ : Type u_2} {s : Set α} {t : Set β} {a : α} [inst : 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 β) :
Prod.swap ⁻¹' s ×ˢ t = t ×ˢ s
@[simp]
theorem Set.image_swap_prod {α : Type u_1} {β : Type u_2} (s : Set α) (t : Set β) :
Prod.swap '' s ×ˢ t = t ×ˢ s
theorem Set.prod_image_image_eq {α : Type u_3} {β : Type u_4} {γ : Type u_1} {δ : Type u_2} {s : Set α} {t : Set β} {m₁ : αγ} {m₂ : βδ} :
(m₁ '' s) ×ˢ (m₂ '' t) = (fun p => (m₁ p.fst, m₂ p.snd)) '' s ×ˢ t
theorem Set.prod_range_range_eq {α : Type u_3} {β : Type u_4} {γ : Type u_1} {δ : Type u_2} {m₁ : αγ} {m₂ : βδ} :
Set.range m₁ ×ˢ Set.range m₂ = Set.range fun p => (m₁ p.fst, m₂ p.snd)
@[simp]
theorem Set.range_prod_map {α : Type u_4} {β : Type u_3} {γ : Type u_1} {δ : Type u_2} {m₁ : αγ} {m₂ : βδ} :
Set.range (Prod.map m₁ m₂) = Set.range m₁ ×ˢ Set.range m₂
theorem Set.prod_range_univ_eq {α : Type u_3} {β : Type u_1} {γ : Type u_2} {m₁ : αγ} :
Set.range m₁ ×ˢ Set.univ = Set.range fun p => (m₁ p.fst, p.snd)
theorem Set.prod_univ_range_eq {α : Type u_1} {β : Type u_3} {δ : Type u_2} {m₂ : βδ} :
Set.univ ×ˢ Set.range m₂ = Set.range fun p => (p.fst, m₂ p.snd)
theorem Set.range_pair_subset {α : Type u_3} {β : Type u_2} {γ : Type u_1} (f : αβ) (g : αγ) :
(Set.range fun x => (f x, g x)) Set.range f ×ˢ Set.range g
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_2} {β : Type u_3} {γ : Type u_1} {s : Set α} {t : Set β} {W : Set γ} {f : α × βγ} :
s ×ˢ t f ⁻¹' W ∀ (a : α) (b : β), a sb tf (a, b) W
theorem Set.image_prod_mk_subset_prod {α : Type u_1} {β : Type u_3} {γ : Type u_2} {f : αβ} {g : αγ} {s : Set α} :
(fun x => (f x, g x)) '' s (f '' s) ×ˢ (g '' s)
theorem Set.image_prod_mk_subset_prod_left {α : Type u_2} {β : Type u_1} {s : Set α} {t : Set β} {b : β} (hb : b t) :
(fun 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) :
Prod.mk a '' t s ×ˢ t
theorem Set.prod_subset_preimage_fst {α : Type u_1} {β : Type u_2} (s : Set α) (t : Set β) :
s ×ˢ t Prod.fst ⁻¹' s
theorem Set.fst_image_prod_subset {α : Type u_1} {β : Type u_2} (s : Set α) (t : Set β) :
Prod.fst '' s ×ˢ t s
theorem Set.fst_image_prod {α : Type u_2} {β : Type u_1} (s : Set β) {t : Set α} (ht : Set.Nonempty t) :
Prod.fst '' s ×ˢ t = s
theorem Set.prod_subset_preimage_snd {α : Type u_1} {β : Type u_2} (s : Set α) (t : Set β) :
s ×ˢ t Prod.snd ⁻¹' t
theorem Set.snd_image_prod_subset {α : Type u_1} {β : Type u_2} (s : Set α) (t : Set β) :
Prod.snd '' s ×ˢ t t
theorem Set.snd_image_prod {α : Type u_1} {β : Type u_2} {s : Set α} (hs : Set.Nonempty s) (t : Set β) :
Prod.snd '' s ×ˢ t = t
theorem Set.prod_diff_prod {α : Type u_1} {β : Type u_2} {s : Set α} {s₁ : Set α} {t : Set β} {t₁ : Set β} :
s ×ˢ t \ s₁ ×ˢ t₁ = s ×ˢ (t \ t₁) (s \ s₁) ×ˢ t
theorem Set.prod_subset_prod_iff {α : Type u_2} {β : Type u_1} {s : Set α} {s₁ : Set α} {t : Set β} {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 : Set α} {s₁ : Set α} {t : Set β} {t₁ : Set β} (h : Set.Nonempty (s ×ˢ t)) :
s ×ˢ t = s₁ ×ˢ t₁ s = s₁ t = t₁
theorem Set.prod_eq_prod_iff {α : Type u_1} {β : Type u_2} {s : Set α} {s₁ : Set α} {t : Set β} {t₁ : Set β} :
s ×ˢ t = s₁ ×ˢ t₁ s = s₁ t = t₁ (s = t = ) (s₁ = t₁ = )
@[simp]
theorem Set.prod_eq_iff_eq {α : Type u_2} {β : Type u_1} {s : Set α} {s₁ : Set α} {t : Set β} (ht : Set.Nonempty t) :
s ×ˢ t = s₁ ×ˢ t s = s₁
theorem Monotone.set_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : 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} [inst : 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 α} [inst : 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 α} [inst : 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 λ 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) Set.diagonal α
@[simp]
theorem Set.mem_diagonal_iff {α : Type u_1} {x : α × α} :
x Set.diagonal α x.fst = x.snd
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 => x) fun x => x) ⁻¹' Set.diagonal α = Set.diagonal s
@[simp]
theorem Set.range_diag {α : Type u_1} :
(Set.range fun x => (x, x)) = Set.diagonal α
theorem Set.diagonal_subset_iff {α : Type u_1} {s : Set (α × α)} :
Set.diagonal α s ∀ (x : α), (x, x) s
@[simp]
@[simp]
theorem Set.diag_preimage_prod {α : Type u_1} (s : Set α) (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 = Set.diagonal α s ×ˢ s
def Set.offDiag {α : Type u_1} (s : Set α) :
Set (α × α)

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

Equations
@[simp]
theorem Set.mem_offDiag {α : Type u_1} {s : Set α} {x : α × α} :
x Set.offDiag s x.fst s x.snd s x.fst x.snd
theorem Set.offDiag_mono {α : Type u_1} :
Monotone Set.offDiag
@[simp]

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 α) :
Set.offDiag s = { x | x s ×ˢ s x.fst x.snd }
@[simp]
@[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.offDiag_inter {α : Type u_1} (s : Set α) (t : Set α) :
theorem Set.offDiag_union {α : Type u_1} {s : Set α} {t : Set α} (h : Disjoint s t) :
theorem Set.offDiag_insert {α : Type u_1} {s : Set α} {a : α} (ha : ¬a s) :

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∈ s.

Equations
@[simp]
theorem Set.mem_pi {ι : Type u_1} {α : ιType u_2} {s : Set ι} {t : (i : ι) → Set (α i)} {f : (i : ι) → α i} :
f Set.pi s 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.pi Set.univ t ∀ (i : ι), f i t i
@[simp]
theorem Set.empty_pi {ι : Type u_2} {α : ιType u_1} (s : (i : ι) → Set (α i)) :
Set.pi s = Set.univ
@[simp]
theorem Set.pi_univ {ι : Type u_1} {α : ιType u_2} (s : Set ι) :
(Set.pi s fun i => Set.univ) = Set.univ
theorem Set.pi_mono {ι : Type u_1} {α : ιType u_2} {s : Set ι} {t₁ : (i : ι) → Set (α i)} {t₂ : (i : ι) → Set (α i)} (h : ∀ (i : ι), i st₁ i t₂ i) :
Set.pi s t₁ Set.pi s t₂
theorem Set.pi_inter_distrib {ι : Type u_1} {α : ιType u_2} {s : Set ι} {t : (i : ι) → Set (α i)} {t₁ : (i : ι) → Set (α i)} :
(Set.pi s fun i => t i t₁ i) = Set.pi s t Set.pi s t₁
theorem Set.pi_congr {ι : Type u_1} {α : ιType u_2} {s₁ : Set ι} {s₂ : Set ι} {t₁ : (i : ι) → Set (α i)} {t₂ : (i : ι) → Set (α i)} (h : s₁ = s₂) (h' : ∀ (i : ι), i s₁t₁ i = t₂ i) :
Set.pi s₁ t₁ = Set.pi s₂ 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 = ) :
theorem Set.univ_pi_eq_empty {ι : Type u_2} {α : ιType u_1} {t : (i : ι) → Set (α i)} {i : ι} (ht : t i = ) :
Set.pi Set.univ t =
theorem Set.pi_nonempty_iff {ι : Type u_1} {α : ιType u_2} {s : Set ι} {t : (i : ι) → Set (α i)} :
Set.Nonempty (Set.pi s t) ∀ (i : ι), x, i sx t i
theorem Set.univ_pi_nonempty_iff {ι : Type u_1} {α : ιType u_2} {t : (i : ι) → Set (α i)} :
Set.Nonempty (Set.pi Set.univ t) ∀ (i : ι), Set.Nonempty (t i)
theorem Set.pi_eq_empty_iff {ι : Type u_1} {α : ιType u_2} {s : Set ι} {t : (i : ι) → Set (α i)} :
Set.pi s 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)} :
Set.pi Set.univ t = i, t i =
@[simp]
theorem Set.univ_pi_empty {ι : Type u_1} {α : ιType u_2} [h : Nonempty ι] :
(Set.pi Set.univ fun x => ) =
@[simp]
theorem Set.disjoint_univ_pi {ι : Type u_2} {α : ιType u_1} {t₁ : (i : ι) → Set (α i)} {t₂ : (i : ι) → Set (α i)} :
Disjoint (Set.pi Set.univ t₁) (Set.pi Set.univ t₂) i, Disjoint (t₁ i) (t₂ i)
theorem Set.range_dcomp {ι : Type u_1} {α : ιType u_3} {β : ιType u_2} (f : (i : ι) → α iβ i) :
(Set.range fun g i => f i (g i)) = Set.pi Set.univ fun i => Set.range (f i)
@[simp]
theorem Set.insert_pi {ι : Type u_1} {α : ιType u_2} (i : ι) (s : Set ι) (t : (i : ι) → Set (α i)) :
@[simp]
theorem Set.singleton_pi {ι : Type u_2} {α : ιType u_1} (i : ι) (t : (i : ι) → Set (α i)) :
theorem Set.singleton_pi' {ι : Type u_2} {α : ιType u_1} (i : ι) (t : (i : ι) → Set (α i)) :
Set.pi {i} t = { x | x i t i }
theorem Set.univ_pi_singleton {ι : Type u_1} {α : ιType u_2} (f : (i : ι) → α i) :
(Set.pi Set.univ fun i => {f i}) = {f}
theorem Set.preimage_pi {ι : Type u_1} {α : ιType u_3} {β : ιType u_2} (s : Set ι) (t : (i : ι) → Set (β i)) (f : (i : ι) → α iβ i) :
(fun g i => f i (g i)) ⁻¹' Set.pi s t = Set.pi s fun i => f i ⁻¹' t i
theorem Set.pi_if {ι : Type u_1} {α : ιType u_2} {p : ιProp} [h : DecidablePred p] (s : Set ι) (t₁ : (i : ι) → Set (α i)) (t₂ : (i : ι) → Set (α i)) :
(Set.pi s fun i => if p i then t₁ i else t₂ i) = Set.pi { i | i s p i } t₁ Set.pi { i | i s ¬p i } t₂
theorem Set.union_pi {ι : Type u_1} {α : ιType u_2} {s₁ : Set ι} {s₂ : Set ι} {t : (i : ι) → Set (α i)} :
Set.pi (s₁ s₂) t = Set.pi s₁ t Set.pi s₂ t
@[simp]
theorem Set.pi_inter_compl {ι : Type u_1} {α : ιType u_2} {t : (i : ι) → Set (α i)} (s : Set ι) :
Set.pi s t Set.pi (s) t = Set.pi Set.univ t
theorem Set.pi_update_of_not_mem {ι : Type u_1} {α : ιType u_3} {β : ιType u_2} {s : Set ι} {i : ι} [inst : DecidableEq ι] (hi : ¬i s) (f : (j : ι) → α j) (a : α i) (t : (j : ι) → α jSet (β j)) :
(Set.pi s fun j => t j (Function.update f i a j)) = Set.pi s fun j => t j (f j)
theorem Set.pi_update_of_mem {ι : Type u_1} {α : ιType u_3} {β : ιType u_2} {s : Set ι} {i : ι} [inst : DecidableEq ι] (hi : i s) (f : (j : ι) → α j) (a : α i) (t : (j : ι) → α jSet (β j)) :
(Set.pi s fun j => t j (Function.update f i a j)) = { x | x i t i a } Set.pi (s \ {i}) fun j => t j (f j)
theorem Set.univ_pi_update {ι : Type u_1} {α : ιType u_3} [inst : DecidableEq ι] {β : ιType u_2} (i : ι) (f : (j : ι) → α j) (a : α i) (t : (j : ι) → α jSet (β j)) :
(Set.pi Set.univ fun j => t j (Function.update f i a j)) = { x | x i t i a } Set.pi ({i}) fun j => t j (f j)
theorem Set.univ_pi_update_univ {ι : Type u_1} {α : ιType u_2} [inst : DecidableEq ι] (i : ι) (s : Set (α i)) :
Set.pi Set.univ (Function.update (fun j => Set.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_2} {α : ιType u_1} {t : (i : ι) → Set (α i)} {i : ι} :
Function.eval i '' Set.pi Set.univ t t i
theorem Set.subset_eval_image_pi {ι : Type u_1} {α : ιType u_2} {s : Set ι} {t : (i : ι) → Set (α i)} (ht : Set.Nonempty (Set.pi s t)) (i : ι) :
theorem Set.eval_image_pi {ι : Type u_1} {α : ιType u_2} {s : Set ι} {t : (i : ι) → Set (α i)} {i : ι} (hs : i s) (ht : Set.Nonempty (Set.pi s t)) :
@[simp]
theorem Set.eval_image_univ_pi {ι : Type u_1} {α : ιType u_2} {t : (i : ι) → Set (α i)} {i : ι} (ht : Set.Nonempty (Set.pi Set.univ t)) :
(fun f => f i) '' Set.pi Set.univ t = t i
theorem Set.pi_subset_pi_iff {ι : Type u_2} {α : ιType u_1} {s : Set ι} {t₁ : (i : ι) → Set (α i)} {t₂ : (i : ι) → Set (α i)} :
Set.pi s t₁ Set.pi s t₂ (∀ (i : ι), i st₁ i t₂ i) Set.pi s t₁ =
theorem Set.univ_pi_subset_univ_pi_iff {ι : Type u_2} {α : ιType u_1} {t₁ : (i : ι) → Set (α i)} {t₂ : (i : ι) → Set (α i)} :
Set.pi Set.univ t₁ Set.pi Set.univ t₂ (∀ (i : ι), t₁ i t₂ i) i, t₁ i =
theorem Set.eval_preimage {ι : Type u_1} {α : ιType u_2} {i : ι} [inst : DecidableEq ι] {s : Set (α i)} :
Function.eval i ⁻¹' s = Set.pi Set.univ (Function.update (fun i => Set.univ) i s)
theorem Set.eval_preimage' {ι : Type u_1} {α : ιType u_2} {i : ι} [inst : DecidableEq ι] {s : Set (α i)} :
Function.eval i ⁻¹' s = Set.pi {i} (Function.update (fun i => Set.univ) i s)
theorem Set.update_preimage_pi {ι : Type u_1} {α : ιType u_2} {s : Set ι} {t : (i : ι) → Set (α i)} {i : ι} [inst : DecidableEq ι] {f : (i : ι) → α i} (hi : i s) (hf : ∀ (j : ι), j sj if j t j) :
theorem Set.update_preimage_univ_pi {ι : Type u_1} {α : ιType u_2} {t : (i : ι) → Set (α i)} {i : ι} [inst : DecidableEq ι] {f : (i : ι) → α i} (hf : ∀ (j : ι), j if j t j) :
Function.update f i ⁻¹' Set.pi Set.univ t = t i
theorem Set.subset_pi_eval_image {ι : Type u_1} {α : ιType u_2} (s : Set ι) (u : Set ((i : ι) → α i)) :
u Set.pi s fun i => Function.eval i '' u
theorem Set.univ_pi_ite {ι : Type u_1} {α : ιType u_2} (s : Set ι) [inst : DecidablePred fun x => x s] (t : (i : ι) → Set (α i)) :
(Set.pi Set.univ fun i => if i s then t i else Set.univ) = Set.pi s t