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

• 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.offDiag: Off-diagonal. s ×ˢ s×ˢ s without the diagonal.
• Set.pi: Arbitrary product of sets.

Cartesian binary product of sets

ink

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

• s ×ˢ t = { p | p.fst ∈ s ∧ p.snd ∈ t }

ink

def Set.«term_×ˢ_» : Lean.TrailingParserDescr

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

Equations

• Set.«term_×ˢ_» = Lean.ParserDescr.trailingNode `Set.term_×ˢ_ 82 83 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ×ˢ ") (Lean.ParserDescr.cat `term 82))

ink

theorem Set.prod_eq {α : Type u_1} {β : Type u_2} (s : Set α) (t : Set β) : s ×ˢ t = Prod.fst ⁻¹' s ∩ Prod.snd ⁻¹' t

ink

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)

ink

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

ink

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)

ink

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

ink

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

• Set.decidableMemProd x = And.decidable

ink

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₂

ink

theorem Set.prod_mono_left {α : Type u_1} {β : Type u_2} {s₁ : Set α} {s₂ : Set α} {t : Set β} (hs : s₁ ⊆ s₂) : s₁ ×ˢ t ⊆ s₂ ×ˢ t

ink

theorem Set.prod_mono_right {α : Type u_2} {β : Type u_1} {s : Set α} {t₁ : Set β} {t₂ : Set β} (ht : t₁ ⊆ t₂) : s ×ˢ t₁ ⊆ s ×ˢ t₂

ink

@[simp]

theorem Set.prod_self_subset_prod_self {α : Type u_1} {s₁ : Set α} {s₂ : Set α} : s₁ ×ˢ s₁ ⊆ s₂ ×ˢ s₂ ↔ s₁ ⊆ s₂

ink

@[simp]

theorem Set.prod_self_ssubset_prod_self {α : Type u_1} {s₁ : Set α} {s₂ : Set α} : s₁ ×ˢ s₁ ⊂ s₂ ×ˢ s₂ ↔ s₁ ⊂ s₂

ink

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

ink

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)

ink

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)

ink

@[simp]

theorem Set.prod_empty {α : Type u_1} {β : Type u_2} {s : Set α} : s ×ˢ ∅ = ∅

ink

@[simp]

theorem Set.empty_prod {α : Type u_1} {β : Type u_2} {t : Set β} : ∅ ×ˢ t = ∅

ink

@[simp]

theorem Set.univ_prod_univ {α : Type u_1} {β : Type u_2} : Set.univ ×ˢ Set.univ = Set.univ

ink

theorem Set.univ_prod {α : Type u_2} {β : Type u_1} {t : Set β} : Set.univ ×ˢ t = Prod.snd ⁻¹' t

ink

theorem Set.prod_univ {α : Type u_1} {β : Type u_2} {s : Set α} : s ×ˢ Set.univ = Prod.fst ⁻¹' s

ink

@[simp]

theorem Set.singleton_prod {α : Type u_1} {β : Type u_2} {t : Set β} {a : α} : {a} ×ˢ t = Prod.mk a '' t

ink

@[simp]

theorem Set.prod_singleton {α : Type u_1} {β : Type u_2} {s : Set α} {b : β} : s ×ˢ {b} = (fun a => (a, b)) '' s

ink

theorem Set.singleton_prod_singleton {α : Type u_1} {β : Type u_2} {a : α} {b : β} : {a} ×ˢ {b} = {(a, b)}

ink

@[simp]

theorem Set.union_prod {α : Type u_1} {β : Type u_2} {s₁ : Set α} {s₂ : Set α} {t : Set β} : (s₁ ∪ s₂) ×ˢ t = s₁ ×ˢ t ∪ s₂ ×ˢ t

ink

@[simp]

theorem Set.prod_union {α : Type u_1} {β : Type u_2} {s : Set α} {t₁ : Set β} {t₂ : Set β} : s ×ˢ (t₁ ∪ t₂) = s ×ˢ t₁ ∪ s ×ˢ t₂

ink

theorem Set.inter_prod {α : Type u_1} {β : Type u_2} {s₁ : Set α} {s₂ : Set α} {t : Set β} : (s₁ ∩ s₂) ×ˢ t = s₁ ×ˢ t ∩ s₂ ×ˢ t

ink

theorem Set.prod_inter {α : Type u_1} {β : Type u_2} {s : Set α} {t₁ : Set β} {t₂ : Set β} : s ×ˢ (t₁ ∩ t₂) = s ×ˢ t₁ ∩ s ×ˢ t₂

ink

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₂)

ink

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₂

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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)

ink

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

ink

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

ink

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

ink

@[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 = ∅

ink

@[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 = ∅

ink

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 ∅

ink

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 ∅

ink

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 ∅

ink

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 ∅

ink

@[simp]

theorem Set.preimage_swap_prod {α : Type u_1} {β : Type u_2} (s : Set α) (t : Set β) : Prod.swap ⁻¹' s ×ˢ t = t ×ˢ s

ink

@[simp]

theorem Set.image_swap_prod {α : Type u_1} {β : Type u_2} (s : Set α) (t : Set β) : Prod.swap '' s ×ˢ t = t ×ˢ s

ink

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

ink

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)

ink

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

ink

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)

ink

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)

ink

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

ink

theorem Set.Nonempty.prod {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} : Set.Nonempty s → Set.Nonempty t → Set.Nonempty (s ×ˢ t)

ink

theorem Set.Nonempty.fst {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} : Set.Nonempty (s ×ˢ t) → Set.Nonempty s

ink

theorem Set.Nonempty.snd {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} : Set.Nonempty (s ×ˢ t) → Set.Nonempty t

ink

theorem Set.prod_nonempty_iff {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} : Set.Nonempty (s ×ˢ t) ↔ Set.Nonempty s ∧ Set.Nonempty t

ink

theorem Set.prod_eq_empty_iff {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} : s ×ˢ t = ∅ ↔ s = ∅ ∨ t = ∅

ink

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 ∈ s → b ∈ t → f (a, b) ∈ W

ink

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)

ink

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

ink

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

ink

theorem Set.prod_subset_preimage_fst {α : Type u_1} {β : Type u_2} (s : Set α) (t : Set β) : s ×ˢ t ⊆ Prod.fst ⁻¹' s

ink

theorem Set.fst_image_prod_subset {α : Type u_1} {β : Type u_2} (s : Set α) (t : Set β) : Prod.fst '' s ×ˢ t ⊆ s

ink

theorem Set.fst_image_prod {α : Type u_2} {β : Type u_1} (s : Set β) {t : Set α} (ht : Set.Nonempty t) : Prod.fst '' s ×ˢ t = s

ink

theorem Set.prod_subset_preimage_snd {α : Type u_1} {β : Type u_2} (s : Set α) (t : Set β) : s ×ˢ t ⊆ Prod.snd ⁻¹' t

ink

theorem Set.snd_image_prod_subset {α : Type u_1} {β : Type u_2} (s : Set α) (t : Set β) : Prod.snd '' s ×ˢ t ⊆ t

ink

theorem Set.snd_image_prod {α : Type u_1} {β : Type u_2} {s : Set α} (hs : Set.Nonempty s) (t : Set β) : Prod.snd '' s ×ˢ t = t

ink

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

ink

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.

ink

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₁

ink

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₁ = ∅)

ink

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

ink

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

ink

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

ink

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

ink

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).

ink

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

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

Equations

• Set.diagonal α = { p | p.fst = p.snd }

ink

theorem Set.mem_diagonal {α : Type u_1} (x : α) : (x, x) ∈ Set.diagonal α

ink

@[simp]

theorem Set.mem_diagonal_iff {α : Type u_1} {x : α × α} : x ∈ Set.diagonal α ↔ x.fst = x.snd

ink

theorem Set.diagonal_nonempty {α : Type u_1} [inst : Nonempty α] : Set.Nonempty (Set.diagonal α)

ink

instance Set.decidableMemDiagonal {α : Type u_1} [h : DecidableEq α] (x : α × α) : Decidable (x ∈ Set.diagonal α)

Equations

• Set.decidableMemDiagonal x = h x.fst x.snd

ink

theorem Set.preimage_coe_coe_diagonal {α : Type u_1} (s : Set α) : (Prod.map (fun x => ↑x) fun x => ↑x) ⁻¹' Set.diagonal α = Set.diagonal ↑s

ink

@[simp]

theorem Set.range_diag {α : Type u_1} : (Set.range fun x => (x, x)) = Set.diagonal α

ink

theorem Set.diagonal_subset_iff {α : Type u_1} {s : Set (α × α)} : Set.diagonal α ⊆ s ↔ ∀ (x : α), (x, x) ∈ s

ink

@[simp]

theorem Set.prod_subset_compl_diagonal_iff_disjoint {α : Type u_1} {s : Set α} {t : Set α} : s ×ˢ t ⊆ Set.diagonal αᶜ ↔ Disjoint s t

ink

@[simp]

theorem Set.diag_preimage_prod {α : Type u_1} (s : Set α) (t : Set α) : (fun x => (x, x)) ⁻¹' s ×ˢ t = s ∩ t

ink

theorem Set.diag_preimage_prod_self {α : Type u_1} (s : Set α) : (fun x => (x, x)) ⁻¹' s ×ˢ s = s

ink

theorem Set.diag_image {α : Type u_1} (s : Set α) : (fun x => (x, x)) '' s = Set.diagonal α ∩ s ×ˢ s

ink

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

• Set.offDiag s = { x | x.fst ∈ s ∧ x.snd ∈ s ∧ x.fst ≠ x.snd }

ink

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

ink

theorem Set.offDiag_mono {α : Type u_1} : Monotone Set.offDiag

ink

@[simp]

theorem Set.offDiag_nonempty {α : Type u_1} {s : Set α} : Set.Nonempty (Set.offDiag s) ↔ Set.Nontrivial s

ink

@[simp]

theorem Set.offDiag_eq_empty {α : Type u_1} {s : Set α} : Set.offDiag s = ∅ ↔ Set.Subsingleton s

ink

theorem Set.Nontrivial.offDiag_nonempty {α : Type u_1} {s : Set α} : Set.Nontrivial s → Set.Nonempty (Set.offDiag s)

Alias of the reverse direction of Set.offDiag_nonempty.

ink

theorem Set.Subsingleton.offDiag_eq_empty {α : Type u_1} {s : Set α} : Set.Nontrivial s → Set.Nonempty (Set.offDiag s)

Alias of the reverse direction of Set.offDiag_nonempty.

ink

theorem Set.offDiag_subset_prod {α : Type u_1} (s : Set α) : Set.offDiag s ⊆ s ×ˢ s

ink

theorem Set.offDiag_eq_sep_prod {α : Type u_1} (s : Set α) : Set.offDiag s = { x | x ∈ s ×ˢ s ∧ x.fst ≠ x.snd }

ink

@[simp]

theorem Set.offDiag_empty {α : Type u_1} : Set.offDiag ∅ = ∅

ink

@[simp]

theorem Set.offDiag_singleton {α : Type u_1} (a : α) : Set.offDiag {a} = ∅

ink

@[simp]

theorem Set.offDiag_univ {α : Type u_1} : Set.offDiag Set.univ = Set.diagonal αᶜ

ink

@[simp]

theorem Set.prod_sdiff_diagonal {α : Type u_1} (s : Set α) : s ×ˢ s \ Set.diagonal α = Set.offDiag s

ink

@[simp]

theorem Set.disjoint_diagonal_offDiag {α : Type u_1} (s : Set α) : Disjoint (Set.diagonal α) (Set.offDiag s)

ink

theorem Set.offDiag_inter {α : Type u_1} (s : Set α) (t : Set α) : Set.offDiag (s ∩ t) = Set.offDiag s ∩ Set.offDiag t

ink

theorem Set.offDiag_union {α : Type u_1} {s : Set α} {t : Set α} (h : Disjoint s t) : Set.offDiag (s ∪ t) = Set.offDiag s ∪ Set.offDiag t ∪ s ×ˢ t ∪ t ×ˢ s

ink

theorem Set.offDiag_insert {α : Type u_1} {s : Set α} {a : α} (ha : ¬a ∈ s) : Set.offDiag (insert a s) = Set.offDiag s ∪ {a} ×ˢ s ∪ s ×ˢ {a}

Cartesian set-indexed product of sets

ink

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

• Set.pi s t = { f | ∀ (i : ι), i ∈ s → f i ∈ t i }

ink

@[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 ∈ s → f i ∈ t i

ink

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

ink

@[simp]

theorem Set.empty_pi {ι : Type u_2} {α : ι → Type u_1} (s : (i : ι) → Set (α i)) : Set.pi ∅ s = Set.univ

ink

@[simp]

theorem Set.pi_univ {ι : Type u_1} {α : ι → Type u_2} (s : Set ι) : (Set.pi s fun i => Set.univ) = Set.univ

ink

theorem Set.pi_mono {ι : Type u_1} {α : ι → Type u_2} {s : Set ι} {t₁ : (i : ι) → Set (α i)} {t₂ : (i : ι) → Set (α i)} (h : ∀ (i : ι), i ∈ s → t₁ i ⊆ t₂ i) : Set.pi s t₁ ⊆ Set.pi s t₂

ink

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₁

ink

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₂

ink

theorem Set.pi_eq_empty {ι : Type u_1} {α : ι → Type u_2} {s : Set ι} {t : (i : ι) → Set (α i)} {i : ι} (hs : i ∈ s) (ht : t i = ∅) : Set.pi s t = ∅

ink

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 = ∅

ink

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 ∈ s → x ∈ t i

ink

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)

ink

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 = ∅

ink

@[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 = ∅

ink

@[simp]

theorem Set.univ_pi_empty {ι : Type u_1} {α : ι → Type u_2} [h : Nonempty ι] : (Set.pi Set.univ fun x => ∅) = ∅

ink

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

ink

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)

ink

@[simp]

theorem Set.insert_pi {ι : Type u_1} {α : ι → Type u_2} (i : ι) (s : Set ι) (t : (i : ι) → Set (α i)) : Set.pi (insert i s) t = Function.eval i ⁻¹' t i ∩ Set.pi s t

ink

@[simp]

theorem Set.singleton_pi {ι : Type u_2} {α : ι → Type u_1} (i : ι) (t : (i : ι) → Set (α i)) : Set.pi {i} t = Function.eval i ⁻¹' t i

ink

theorem Set.singleton_pi' {ι : Type u_2} {α : ι → Type u_1} (i : ι) (t : (i : ι) → Set (α i)) : Set.pi {i} t = { x | x i ∈ t i }

ink

theorem Set.univ_pi_singleton {ι : Type u_1} {α : ι → Type u_2} (f : (i : ι) → α i) : (Set.pi Set.univ fun i => {f i}) = {f}

ink

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

ink

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₂

ink

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

ink

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

ink

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 : ι) → α j → Set (β j)) : (Set.pi s fun j => t j (Function.update f i a j)) = Set.pi s fun j => t j (f j)

ink

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 : ι) → α j → Set (β 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)

ink

theorem Set.univ_pi_update {ι : Type u_1} {α : ι → Type u_3} [inst : DecidableEq ι] {β : ι → Type u_2} (i : ι) (f : (j : ι) → α j) (a : α i) (t : (j : ι) → α j → Set (β 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)

ink

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

ink

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 '' Set.pi s t ⊆ t i

ink

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

ink

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 : ι) : t i ⊆ Function.eval i '' Set.pi s t

ink

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)) : Function.eval i '' Set.pi s t = t i

ink

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

ink

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 ∈ s → t₁ i ⊆ t₂ i) ∨ Set.pi s t₁ = ∅

ink

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 = ∅

ink

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)

ink

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)

ink

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 ∈ s → j ≠ i → f j ∈ t j) : Function.update f i ⁻¹' Set.pi s t = t i

ink

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 ≠ i → f j ∈ t j) : Function.update f i ⁻¹' Set.pi Set.univ t = t i

ink

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

ink

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