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 #

@[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
theorem set.prod_eq {α : Type u_1} {β : Type u_2} (s : set α) (t : set β) :
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)
@[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
@[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)
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
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₂
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
theorem set.forall_prod_set {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} {p : α × β → Prop} :
(∀ (x : α × β), x s.prod 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 : α × β) (H : x s.prod 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}.prod t = prod.mk a '' t
@[simp]
theorem set.prod_singleton {α : Type u_1} {β : Type u_2} {s : set α} {b : β} :
s.prod {b} = (λ (a : α), (a, b)) '' s
theorem set.singleton_prod_singleton {α : Type u_1} {β : Type u_2} {a : α} {b : β} :
{a}.prod {b} = {(a, b)}
@[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
@[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₂
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₂)
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
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
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
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
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
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)
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
@[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
@[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 : b t) :
(λ (a : α), (a, b)) ⁻¹' s.prod 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.prod 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)] :
prod.mk a ⁻¹' s.prod 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.prod 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.prod t = ite (a s) (g ⁻¹' t)
theorem set.preimage_swap_prod {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} :
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).prod (m₂ '' t) = (λ (p : α × β), (m₁ p.fst, m₂ p.snd)) '' s.prod t
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))
@[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₂)
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))
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))
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)
theorem set.nonempty.prod {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} :
s.nonemptyt.nonempty(s.prod t).nonempty
theorem set.nonempty.fst {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} :
(s.prod t).nonempty → s.nonempty
theorem set.nonempty.snd {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} :
(s.prod t).nonempty → t.nonempty
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.prod 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.prod t f ⁻¹' W ∀ (a : α) (b : β), a sb tf (a, b) W
theorem set.fst_image_prod_subset {α : Type u_1} {β : Type u_2} (s : set α) (t : set β) :
theorem set.prod_subset_preimage_fst {α : 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.snd_image_prod_subset {α : 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 {α : 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.prod t \ s₁.prod t₁ = s.prod (t \ t₁) (s \ s₁).prod t
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.

@[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 #

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

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

Equations
@[simp]
theorem set.mem_diagonal {α : Type u_1} (x : α) :
(x, x) set.diagonal α
theorem set.diagonal_eq_range {α : Type u_1} :
set.diagonal α = set.range (λ (x : α), (x, x))

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
  • s.pi t = {f : Π (i : ι), α i | ∀ (i : ι), i sf i t i}
@[simp]
theorem set.mem_pi {ι : Type u_1} {α : ι → Type u_2} {s : set ι} {t : Π (i : ι), set (α i)} {f : Π (i : ι), α i} :
f s.pi t ∀ (i : ι), i sf i t i
@[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
@[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 st₁ 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 sx 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 =
theorem set.univ_pi_eq_empty_iff {ι : Type u_1} {α : ι → Type u_2} {t : Π (i : ι), set (α i)} :
set.univ.pi t = ∃ (i : ι), t i =
@[simp]
theorem set.univ_pi_empty {ι : Type u_1} {α : ι → Type u_2} [h : nonempty ι] :
set.univ.pi (λ (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)) :
(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)) :
{i}.pi t = function.eval i ⁻¹' 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.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 = set.univ.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 : ι), α jset (β j)) :
s.pi (λ (j : ι), t j (function.update f 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 : ι), α jset (β 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))
theorem set.univ_pi_update {ι : Type u_1} {α : ι → Type u_2} [decidable_eq ι] {β : ι → Type u_3} (i : ι) (f : Π (j : ι), α j) (a : α i) (t : Π (j : ι), α jset (β 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))
theorem set.univ_pi_update_univ {ι : Type u_1} {α : ι → Type u_2} [decidable_eq ι] (i : ι) (s : set (α 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
@[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
theorem set.eval_preimage {ι : Type u_1} {α : ι → Type u_2} {i : ι} [decidable_eq ι] {s : set (α i)} :
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)
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 sj if j t j) :
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 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 (λ (i : ι), function.eval 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