scilib documentation

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 #

Cartesian binary product of sets #

source
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
source
theorem set.prod_eq {α : Type u_1} {β : Type u_2} (s : set α) (t : set β) :
s ×ˢ 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 ×ˢ 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 ×ˢ 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 ×ˢ 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 ×ˢ t
source
@[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
source
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₂
source
theorem set.prod_mono_left {α : Type u_1} {β : Type u_2} {s₁ s₂ : set α} {t : set β} (hs : s₁ ⊆ s₂) :
s₁ ×ˢ t ⊆ s₂ ×ˢ t
source
theorem set.prod_mono_right {α : Type u_1} {β : Type u_2} {s : set α} {t₁ t₂ : set β} (ht : t₁ ⊆ t₂) :
s ×ˢ t₁ ⊆ s ×ˢ t₂
source
@[simp]
theorem set.prod_self_subset_prod_self {α : Type u_1} {s₁ s₂ : set α} :
s₁ ×ˢ s₁ ⊆ s₂ ×ˢ s₂ ↔ s₁ ⊆ s₂
source
@[simp]
theorem set.prod_self_ssubset_prod_self {α : Type u_1} {s₁ s₂ : set α} :
s₁ ×ˢ s₁ ⊂ s₂ ×ˢ s₂ ↔ s₁ ⊂ s₂
source
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
source
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)
source
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)
source
@[simp]
theorem set.prod_empty {α : Type u_1} {β : Type u_2} {s : set α} :
s ×ˢ ∅ = ∅
source
@[simp]
theorem set.empty_prod {α : Type u_1} {β : Type u_2} {t : set β} :
∅ ×ˢ t = ∅
source
@[simp]
theorem set.univ_prod_univ {α : Type u_1} {β : Type u_2} :
set.univ ×ˢ set.univ = set.univ
source
theorem set.univ_prod {α : Type u_1} {β : Type u_2} {t : set β} :
set.univ ×ˢ t = prod.snd ⁻¹' t
source
theorem set.prod_univ {α : Type u_1} {β : Type u_2} {s : set α} :
s ×ˢ set.univ = prod.fst ⁻¹' s
source
@[simp]
theorem set.singleton_prod {α : Type u_1} {β : Type u_2} {t : set β} {a : α} :
{a} ×ˢ t = prod.mk a '' t
source
@[simp]
theorem set.prod_singleton {α : Type u_1} {β : Type u_2} {s : set α} {b : β} :
s ×ˢ {b} = (λ (a : α), (a, b)) '' s
source
theorem set.singleton_prod_singleton {α : Type u_1} {β : Type u_2} {a : α} {b : β} :
{a} ×ˢ {b} = {(a, b)}
source
@[simp]
theorem set.union_prod {α : Type u_1} {β : Type u_2} {s₁ s₂ : set α} {t : set β} :
(s₁ ∪ s₂) ×ˢ t = s₁ ×ˢ t ∪ s₂ ×ˢ t
source
@[simp]
theorem set.prod_union {α : Type u_1} {β : Type u_2} {s : set α} {t₁ t₂ : set β} :
s ×ˢ (t₁ ∪ t₂) = s ×ˢ t₁ ∪ s ×ˢ t₂
source
theorem set.inter_prod {α : Type u_1} {β : Type u_2} {s₁ s₂ : set α} {t : set β} :
(s₁ ∩ s₂) ×ˢ t = s₁ ×ˢ t ∩ s₂ ×ˢ t
source
theorem set.prod_inter {α : Type u_1} {β : Type u_2} {s : set α} {t₁ t₂ : set β} :
s ×ˢ (t₁ ∩ t₂) = s ×ˢ t₁ ∩ s ×ˢ t₂
source
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₂)
source
@[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₂
source
theorem 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₂)
source
theorem 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₂)
source
theorem set.insert_prod {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} {a : α} :
has_insert.insert a s ×ˢ t = prod.mk a '' t ∪ s ×ˢ t
source
theorem set.prod_insert {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} {b : β} :
s ×ˢ has_insert.insert b t = (λ (a : α), (a, b)) '' s ∪ s ×ˢ 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) ×ˢ (g ⁻¹' t) = (λ (p : γ × δ), (f p.fst, g p.snd)) ⁻¹' s ×ˢ t
source
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
source
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
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 ×ˢ t = (f ⁻¹' s) ×ˢ (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 ×ˢ 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 ×ˢ 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 ×ˢ 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 ×ˢ 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 ×ˢ 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 ×ˢ 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 ×ˢ 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 ×ˢ 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 ×ˢ t = ite (a ∈ s) (g ⁻¹' t) ∅
source
@[simp]
theorem set.preimage_swap_prod {α : Type u_1} {β : Type u_2} (s : set α) (t : set β) :
prod.swap ⁻¹' s ×ˢ t = t ×ˢ s
source
@[simp]
theorem set.image_swap_prod {α : Type u_1} {β : Type u_2} (s : set α) (t : set β) :
prod.swap '' s ×ˢ t = t ×ˢ s
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) ×ˢ (m₂ '' t) = (λ (p : α × β), (m₁ p.fst, m₂ p.snd)) '' s ×ˢ 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₁ ×ˢ 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₁ ×ˢ set.range m₂
source
theorem set.prod_range_univ_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m₁ : α → γ} :
set.range m₁ ×ˢ 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 ×ˢ 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 ×ˢ set.range g
source
theorem set.nonempty.prod {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} :
s.nonempty → t.nonempty → (s ×ˢ t).nonempty
source
theorem set.nonempty.fst {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} :
(s ×ˢ t).nonempty → s.nonempty
source
theorem set.nonempty.snd {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} :
(s ×ˢ t).nonempty → t.nonempty
source
theorem set.prod_nonempty_iff {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} :
(s ×ˢ t).nonempty ↔ s.nonempty ∧ t.nonempty
source
theorem set.prod_eq_empty_iff {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} :
s ×ˢ 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 ×ˢ t ⊆ f ⁻¹' W ↔ ∀ (a : α) (b : β), a ∈ s → b ∈ t → f (a, b) ∈ W
source
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)
source
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
source
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
source
theorem set.prod_subset_preimage_fst {α : Type u_1} {β : Type u_2} (s : set α) (t : set β) :
s ×ˢ t ⊆ prod.fst ⁻¹' s
source
theorem set.fst_image_prod_subset {α : Type u_1} {β : Type u_2} (s : set α) (t : set β) :
prod.fst '' s ×ˢ t ⊆ s
source
theorem set.fst_image_prod {α : Type u_1} {β : Type u_2} (s : set β) {t : set α} (ht : t.nonempty) :
prod.fst '' s ×ˢ t = s
source
theorem set.prod_subset_preimage_snd {α : Type u_1} {β : Type u_2} (s : set α) (t : set β) :
s ×ˢ t ⊆ prod.snd ⁻¹' t
source
theorem set.snd_image_prod_subset {α : Type u_1} {β : Type u_2} (s : set α) (t : set β) :
prod.snd '' s ×ˢ t ⊆ t
source
theorem set.snd_image_prod {α : Type u_1} {β : Type u_2} {s : set α} (hs : s.nonempty) (t : set β) :
prod.snd '' s ×ˢ t = t
source
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
source
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.

source
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₁
source
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₁ = ∅)
source
@[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₁
source
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)
source
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)
source
theorem monotone_on.set_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : set α} [preorder α] {f : α → set β} {g : α → set γ} (hf : monotone_on f s) (hg : monotone_on g s) :
monotone_on (λ (x : α), f x ×ˢ g x) s
source
theorem antitone_on.set_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : set α} [preorder α] {f : α → set β} {g : α → set γ} (hf : antitone_on f s) (hg : antitone_on g 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).

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

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

Equations
source
theorem set.mem_diagonal {α : Type u_1} (x : α) :
(x, x) ∈ set.diagonal α
source
@[simp]
theorem set.mem_diagonal_iff {α : Type u_1} {x : α × α} :
x ∈ set.diagonal α ↔ x.fst = x.snd
source
theorem set.diagonal_nonempty {α : Type u_1} [nonempty α] :
(set.diagonal α).nonempty
source
@[protected, instance]
def set.decidable_mem_diagonal {α : Type u_1} [h : decidable_eq α] (x : α × α) :
decidable (x ∈ set.diagonal α)
Equations
source
theorem set.preimage_coe_coe_diagonal {α : Type u_1} (s : set α) :
prod.map coe coe ⁻¹' set.diagonal α = set.diagonal ↥s
source
@[simp]
theorem set.range_diag {α : Type u_1} :
set.range (λ (x : α), (x, x)) = set.diagonal α
source
theorem set.diagonal_subset_iff {α : Type u_1} {s : set (α × α)} :
set.diagonal α ⊆ s ↔ ∀ (x : α), (x, x) ∈ s
source
@[simp]
theorem set.prod_subset_compl_diagonal_iff_disjoint {α : Type u_1} {s t : set α} :
s ×ˢ t ⊆ (set.diagonal α)ᶜ ↔ disjoint s t
source
@[simp]
theorem set.diag_preimage_prod {α : Type u_1} (s t : set α) :
(λ (x : α), (x, x)) ⁻¹' s ×ˢ t = s ∩ t
source
theorem set.diag_preimage_prod_self {α : Type u_1} (s : set α) :
(λ (x : α), (x, x)) ⁻¹' s ×ˢ s = s
source
theorem set.diag_image {α : Type u_1} (s : set α) :
(λ (x : α), (x, x)) '' s = set.diagonal α ∩ s ×ˢ s
source
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
source
@[simp]
theorem set.mem_off_diag {α : Type u_1} {s : set α} {x : α × α} :
x ∈ s.off_diag ↔ x.fst ∈ s ∧ x.snd ∈ s ∧ x.fst ≠ x.snd
source
theorem set.off_diag_mono {α : Type u_1} :
monotone set.off_diag
source
@[simp]
theorem set.off_diag_nonempty {α : Type u_1} {s : set α} :
s.off_diag.nonempty ↔ s.nontrivial
source
@[simp]
theorem set.off_diag_eq_empty {α : Type u_1} {s : set α} :
s.off_diag = ∅ ↔ s.subsingleton
source
theorem set.nontrivial.off_diag_nonempty {α : Type u_1} {s : set α} :
s.nontrivial → s.off_diag.nonempty

Alias of the reverse direction of set.off_diag_nonempty.

source
theorem set.subsingleton.off_diag_eq_empty {α : Type u_1} {s : set α} :
s.nontrivial → s.off_diag.nonempty

Alias of the reverse direction of set.off_diag_nonempty.

source
theorem set.off_diag_subset_prod {α : Type u_1} (s : set α) :
s.off_diag ⊆ s ×ˢ s
source
theorem set.off_diag_eq_sep_prod {α : Type u_1} (s : set α) :
s.off_diag = {x ∈ s ×ˢ s | x.fst ≠ x.snd}
source
@[simp]
theorem set.off_diag_empty {α : Type u_1} :
∅.off_diag = ∅
source
@[simp]
theorem set.off_diag_singleton {α : Type u_1} (a : α) :
{a}.off_diag = ∅
source
@[simp]
theorem set.off_diag_univ {α : Type u_1} :
set.univ.off_diag = (set.diagonal α)ᶜ
source
@[simp]
theorem set.prod_sdiff_diagonal {α : Type u_1} (s : set α) :
s ×ˢ s \ set.diagonal α = s.off_diag
source
@[simp]
theorem set.disjoint_diagonal_off_diag {α : Type u_1} (s : set α) :
disjoint (set.diagonal α) s.off_diag
source
theorem set.off_diag_inter {α : Type u_1} (s t : set α) :
(s ∩ t).off_diag = s.off_diag ∩ t.off_diag
source
theorem set.off_diag_union {α : Type u_1} {s t : set α} (h : disjoint s t) :
(s ∪ t).off_diag = s.off_diag ∪ t.off_diag ∪ s ×ˢ t ∪ t ×ˢ s
source
theorem set.off_diag_insert {α : Type u_1} {s : set α} {a : α} (ha : a ∉ s) :
(has_insert.insert a s).off_diag = s.off_diag ∪ {a} ×ˢ s ∪ s ×ˢ {a}

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}
Instances for set.pi
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
@[simp]
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.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)
source
theorem 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₂)
source
theorem set.pi_eq_empty_iff' {ι : Type u_1} {α : ι → Type u_2} {s : set ι} {t : Π (i : ι), set (α i)} [∀ (i : ι), nonempty (α i)] :
s.pi t = ∅ ↔ ∃ (i : ι) (H : i ∈ s), t i = ∅
source
@[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₂) ↔ ∃ (i : ι) (H : i ∈ s), disjoint (t₁ i) (t₂ 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)) :
(has_insert.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.univ_pi_singleton {ι : Type u_1} {α : ι → Type u_2} (f : Π (i : ι), α i) :
set.univ.pi (λ (i : ι), {f i}) = {f}
source
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)
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_subset {ι : Type u_1} {α : ι → Type u_2} {s : set ι} {t : Π (i : ι), set (α i)} {i : ι} (hs : i ∈ s) :
function.eval i '' s.pi t ⊆ t i
source
theorem set.eval_image_univ_pi_subset {ι : Type u_1} {α : ι → Type u_2} {t : Π (i : ι), set (α i)} {i : ι} :
function.eval i '' set.univ.pi t ⊆ t i
source
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 ⊆ function.eval i '' s.pi t
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.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₁ = ∅
source
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 = ∅
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