mathlib documentation

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 #

source
@[protected]
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
source
theorem set.prod_eq {α : Type u_1} {β : Type u_2} (s : set α) (t : set β) :
s.prod t = prod.fst ⁻¹' s ∩ prod.snd ⁻¹' t
source
theorem set.mem_prod_eq {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} {p : α × β} :
p ∈ s.prod t = (p.fst ∈ s ∧ p.snd ∈ t)
source
@[simp]
theorem set.mem_prod {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} {p : α × β} :
p ∈ s.prod t ↔ p.fst ∈ s ∧ p.snd ∈ t
source
@[simp]
theorem set.prod_mk_mem_set_prod_eq {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} {a : α} {b : β} :
(a, b) ∈ s.prod t = (a ∈ s ∧ b ∈ t)
source
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.prod t
source
theorem set.prod_mono {α : Type u_1} {β : Type u_2} {s₁ s₂ : set α} {t₁ t₂ : set β} (hs : s₁ ⊆ s₂) (ht : t₁ ⊆ t₂) :
s₁.prod t₁ ⊆ s₂.prod t₂
source
theorem set.prod_subset_iff {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} {P : set (α × β)} :
s.prod t ⊆ P ↔ ∀ (x : α), x ∈ s → ∀ (y : β), y ∈ t → (x, y) ∈ P
source
theorem set.forall_prod_set {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} {p : α × β → Prop} :
(∀ (x : α × β), x ∈ s.prod t → p x) ↔ ∀ (x : α), x ∈ s → ∀ (y : β), y ∈ t → p (x, y)
source
theorem set.exists_prod_set {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} {p : α × β → Prop} :
(∃ (x : α × β) (H : x ∈ s.prod t), p x) ↔ ∃ (x : α) (H : x ∈ s) (y : β) (H : y ∈ t), p (x, y)
source
@[simp]
theorem set.prod_empty {α : Type u_1} {β : Type u_2} {s : set α} :
s.prod ∅ = ∅
source
@[simp]
theorem set.empty_prod {α : Type u_1} {β : Type u_2} {t : set β} :
∅.prod t = ∅
source
@[simp]
theorem set.univ_prod_univ {α : Type u_1} {β : Type u_2} :
set.univ.prod set.univ = set.univ
source
theorem set.univ_prod {α : Type u_1} {β : Type u_2} {t : set β} :
set.univ.prod t = prod.snd ⁻¹' t
source
theorem set.prod_univ {α : Type u_1} {β : Type u_2} {s : set α} :
s.prod set.univ = prod.fst ⁻¹' s
source
@[simp]
theorem set.singleton_prod {α : Type u_1} {β : Type u_2} {t : set β} {a : α} :
{a}.prod t = prod.mk a '' t
source
@[simp]
theorem set.prod_singleton {α : Type u_1} {β : Type u_2} {s : set α} {b : β} :
s.prod {b} = (λ (a : α), (a, b)) '' s
source
theorem set.singleton_prod_singleton {α : Type u_1} {β : Type u_2} {a : α} {b : β} :
{a}.prod {b} = {(a, b)}
source
@[simp]
theorem set.union_prod {α : Type u_1} {β : Type u_2} {s₁ s₂ : set α} {t : set β} :
(s₁ ∪ s₂).prod t = s₁.prod t ∪ s₂.prod t
source
@[simp]
theorem set.prod_union {α : Type u_1} {β : Type u_2} {s : set α} {t₁ t₂ : set β} :
s.prod (t₁ ∪ t₂) = s.prod t₁ ∪ s.prod t₂
source
theorem set.prod_inter_prod {α : Type u_1} {β : Type u_2} {s₁ s₂ : set α} {t₁ t₂ : set β} :
s₁.prod t₁ ∩ s₂.prod t₂ = (s₁ ∩ s₂).prod (t₁ ∩ t₂)
source
theorem set.insert_prod {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} {a : α} :
(insert a s).prod t = prod.mk a '' t ∪ s.prod t
source
theorem set.prod_insert {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} {b : β} :
s.prod (insert b t) = (λ (a : α), (a, b)) '' s ∪ s.prod t
source
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).prod (g ⁻¹' t) = (λ (p : γ × δ), (f p.fst, g p.snd)) ⁻¹' s.prod t
source
theorem set.prod_preimage_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : set α} {t : set β} {f : γ → α} :
(f ⁻¹' s).prod t = (λ (p : γ × β), (f p.fst, p.snd)) ⁻¹' s.prod t
source
theorem set.prod_preimage_right {α : Type u_1} {β : Type u_2} {δ : Type u_4} {s : set α} {t : set β} {g : δ → β} :
s.prod (g ⁻¹' t) = (λ (p : α × δ), (p.fst, g p.snd)) ⁻¹' s.prod t
source
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.prod t = (f ⁻¹' s).prod (g ⁻¹' t)
source
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.prod t = f ⁻¹' s ∩ g ⁻¹' t
source
@[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.prod t = s
source
@[simp]
theorem set.mk_preimage_prod_right {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} {a : α} (ha : a ∈ s) :
prod.mk a ⁻¹' s.prod t = t
source
@[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.prod t = ∅
source
@[simp]
theorem set.mk_preimage_prod_right_eq_empty {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} {a : α} (ha : a ∉ s) :
prod.mk a ⁻¹' s.prod t = ∅
source
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.prod t = ite (b ∈ t) s ∅
source
theorem set.mk_preimage_prod_right_eq_if {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} {a : α} [decidable_pred (λ (_x : α), _x ∈ s)] :
prod.mk a ⁻¹' s.prod t = ite (a ∈ s) t ∅
source
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.prod t = ite (b ∈ t) (f ⁻¹' s) ∅
source
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.prod t = ite (a ∈ s) (g ⁻¹' t) ∅
source
theorem set.preimage_swap_prod {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} :
prod.swap ⁻¹' t.prod s = s.prod t
source
theorem set.image_swap_prod {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} :
prod.swap '' t.prod s = s.prod t
source
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).prod (m₂ '' t) = (λ (p : α × β), (m₁ p.fst, m₂ p.snd)) '' s.prod t
source
theorem set.prod_range_range_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {m₁ : α → γ} {m₂ : β → δ} :
(set.range m₁).prod (set.range m₂) = set.range (λ (p : α × β), (m₁ p.fst, m₂ p.snd))
source
@[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₂) = (set.range m₁).prod (set.range m₂)
source
theorem set.prod_range_univ_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m₁ : α → γ} :
(set.range m₁).prod set.univ = set.range (λ (p : α × β), (m₁ p.fst, p.snd))
source
theorem set.prod_univ_range_eq {α : Type u_1} {β : Type u_2} {δ : Type u_4} {m₂ : β → δ} :
set.univ.prod (set.range m₂) = set.range (λ (p : α × β), (p.fst, m₂ p.snd))
source
theorem set.range_pair_subset {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β) (g : α → γ) :
set.range (λ (x : α), (f x, g x)) ⊆ (set.range f).prod (set.range g)
source
theorem set.nonempty.prod {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} :
s.nonempty → t.nonempty → (s.prod t).nonempty
source
theorem set.nonempty.fst {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} :
(s.prod t).nonempty → s.nonempty
source
theorem set.nonempty.snd {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} :
(s.prod t).nonempty → t.nonempty
source
theorem set.prod_nonempty_iff {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} :
(s.prod t).nonempty ↔ s.nonempty ∧ t.nonempty
source
theorem set.prod_eq_empty_iff {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} :
s.prod t = ∅ ↔ s = ∅ ∨ t = ∅
source
theorem set.prod_sub_preimage_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : set α} {t : set β} {W : set γ} {f : α × β → γ} :
s.prod t ⊆ f ⁻¹' W ↔ ∀ (a : α) (b : β), a ∈ s → b ∈ t → f (a, b) ∈ W
source
theorem set.fst_image_prod_subset {α : Type u_1} {β : Type u_2} (s : set α) (t : set β) :
prod.fst '' s.prod t ⊆ s
source
theorem set.prod_subset_preimage_fst {α : Type u_1} {β : Type u_2} (s : set α) (t : set β) :
s.prod t ⊆ prod.fst ⁻¹' s
source
theorem set.fst_image_prod {α : Type u_1} {β : Type u_2} (s : set β) {t : set α} (ht : t.nonempty) :
prod.fst '' s.prod t = s
source
theorem set.snd_image_prod_subset {α : Type u_1} {β : Type u_2} (s : set α) (t : set β) :
prod.snd '' s.prod t ⊆ t
source
theorem set.prod_subset_preimage_snd {α : Type u_1} {β : Type u_2} (s : set α) (t : set β) :
s.prod t ⊆ prod.snd ⁻¹' t
source
theorem set.snd_image_prod {α : Type u_1} {β : Type u_2} {s : set α} (hs : s.nonempty) (t : set β) :
prod.snd '' s.prod t = t
source
theorem set.prod_diff_prod {α : Type u_1} {β : Type u_2} {s s₁ : set α} {t t₁ : set β} :
s.prod t \ s₁.prod t₁ = s.prod (t \ t₁) ∪ (s \ s₁).prod t
source
theorem set.prod_subset_prod_iff {α : Type u_1} {β : Type u_2} {s s₁ : set α} {t t₁ : set β} :
s.prod t ⊆ s₁.prod 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.

source
@[simp]
theorem set.image_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : set α} {t : set β} (f : α → β → γ) :
(λ (x : α × β), f x.fst x.snd) '' s.prod t = set.image2 f s t

Diagonal #

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

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

Equations
source
@[simp]
theorem set.mem_diagonal {α : Type u_1} (x : α) :
(x, x) ∈ set.diagonal α
source
theorem set.preimage_coe_coe_diagonal {α : Type u_1} (s : set α) :
prod.map coe coe ⁻¹' set.diagonal α = set.diagonal ↥s
source
theorem set.diagonal_eq_range {α : Type u_1} :
set.diagonal α = set.range (λ (x : α), (x, x))

Cartesian set-indexed product of sets #

source
def set.pi {ι : Type u_1} {α : ι → Type u_2} (s : set ι) (t : Π (i : ι), set (α i)) :
set (Π (i : ι), α i)

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

Equations
  • s.pi t = {f : Π (i : ι), α i | ∀ (i : ι), i ∈ s → f i ∈ t i}
source
@[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
source
@[simp]
theorem set.mem_univ_pi {ι : Type u_1} {α : ι → Type u_2} {t : Π (i : ι), set (α i)} {f : Π (i : ι), α i} :
f ∈ set.univ.pi t ↔ ∀ (i : ι), f i ∈ t i
source
@[simp]
theorem set.empty_pi {ι : Type u_1} {α : ι → Type u_2} (s : Π (i : ι), set (α i)) :
∅.pi s = set.univ
source
@[simp]
theorem set.pi_univ {ι : Type u_1} {α : ι → Type u_2} (s : set ι) :
s.pi (λ (i : ι), set.univ) = set.univ
source
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₂
source
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₁
source
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₂
source
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 = ∅
source
theorem set.univ_pi_eq_empty {ι : Type u_1} {α : ι → Type u_2} {t : Π (i : ι), set (α i)} {i : ι} (ht : t i = ∅) :
set.univ.pi t = ∅
source
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
source
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
source
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 = ∅
source
theorem set.univ_pi_eq_empty_iff {ι : Type u_1} {α : ι → Type u_2} {t : Π (i : ι), set (α i)} :
set.univ.pi t = ∅ ↔ ∃ (i : ι), t i = ∅
source
@[simp]
theorem set.univ_pi_empty {ι : Type u_1} {α : ι → Type u_2} [h : nonempty ι] :
set.univ.pi (λ (i : ι), ∅) = ∅
source
@[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))
source
@[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
source
@[simp]
theorem set.singleton_pi {ι : Type u_1} {α : ι → Type u_2} (i : ι) (t : Π (i : ι), set (α i)) :
{i}.pi t = function.eval i ⁻¹' t i
source
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}
source
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₂
source
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
source
@[simp]
theorem set.pi_inter_compl {ι : Type u_1} {α : ι → Type u_2} {t : Π (i : ι), set (α i)} (s : set ι) :
s.pi t ∩ sᶜ.pi t = set.univ.pi t
source
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 (function.update f i a j)) = s.pi (λ (j : ι), t j (f j))
source
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 (function.update f i a j)) = {x : Π (i : ι), β i | x i ∈ t i a} ∩ (s \ {i}).pi (λ (j : ι), t j (f j))
source
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 (function.update f i a j)) = {x : Π (i : ι), β i | x i ∈ t i a} ∩ {i}ᶜ.pi (λ (j : ι), t j (f j))
source
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) = function.eval i ⁻¹' s
source
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
source
@[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) '' set.univ.pi t = t i
source
theorem set.eval_preimage {ι : Type u_1} {α : ι → Type u_2} {i : ι} [decidable_eq ι] {s : set (α i)} :
function.eval i ⁻¹' s = set.univ.pi (function.update (λ (i : ι), set.univ) i s)
source
theorem set.eval_preimage' {ι : Type u_1} {α : ι → Type u_2} {i : ι} [decidable_eq ι] {s : set (α i)} :
function.eval i ⁻¹' s = {i}.pi (function.update (λ (i : ι), set.univ) i s)
source
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) :
function.update f i ⁻¹' s.pi t = t i
source
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) :
function.update f i ⁻¹' set.univ.pi t = t i
source
theorem set.subset_pi_eval_image {ι : Type u_1} {α : ι → Type u_2} (s : set ι) (u : set (Π (i : ι), α i)) :
u ⊆ s.pi (λ (i : ι), function.eval i '' u)
source
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