Sets in product and pi types

This file proves basic properties of product of sets in α × β and in Π i, α i, and of the diagonal of a type.

Main declarations

This file contains basic results on the following notions, which are defined in Set.Operations.

• Set.prod: Binary product of sets. For s : Set α, t : Set β, we have s.prod t : Set (α × β). Denoted by s ×ˢ t.
• Set.diagonal: Diagonal of a type. Set.diagonal α = {(x, x) | x : α}.
• Set.offDiag: Off-diagonal. s ×ˢ s without the diagonal.
• Set.pi: Arbitrary product of sets.

Cartesian binary product of sets

theorem Set.Subsingleton.prod {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} (hs : s.Subsingleton) (ht : t.Subsingleton) : (s ×ˢ t).Subsingleton

instance Set.decidableMemProd {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} [DecidablePred fun (x : α) => x ∈ s] [DecidablePred fun (x : β) => x ∈ t] : DecidablePred fun (x : α × β) => x ∈ s ×ˢ t

Equations

• Set.decidableMemProd x = inferInstanceAs (Decidable (x.1 ∈ s ∧ x.2 ∈ t))

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₂

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

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

Alias of Set.prod_mono_left.

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

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

Alias of Set.prod_mono_right.

@[simp]

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

@[simp]

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

theorem Set.prod_subset_iff {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {P : Set (α × β)} : s ×ˢ t ⊆ P ↔ ∀ x ∈ s, ∀ y ∈ t, (x, y) ∈ P

theorem Set.forall_prod_set {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {p : α × β → Prop} : (∀ x ∈ s ×ˢ t, p x) ↔ ∀ x ∈ s, ∀ y ∈ t, p (x, y)

theorem Set.exists_prod_set {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {p : α × β → Prop} : (∃ x ∈ s ×ˢ t, p x) ↔ ∃ x ∈ s, ∃ y ∈ t, p (x, y)

@[simp]

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

@[simp]

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

@[simp]

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

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

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

@[simp]

theorem Set.prod_eq_univ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} [Nonempty α] [Nonempty β] : s ×ˢ t = univ ↔ s = univ ∧ t = univ

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

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

@[simp]

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₁ 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₁ t₂ : Set β} : s ×ˢ (t₁ ∪ t₂) = s ×ˢ t₁ ∪ s ×ˢ t₂

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

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

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

theorem Set.compl_prod_eq_union {α : Type u_5} {β : Type u_6} (s : Set α) (t : Set β) : (s ×ˢ t)ᶜ = sᶜ ×ˢ univ ∪ univ ×ˢ tᶜ

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

theorem Set.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₂)

theorem Set.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₂)

theorem Set.prodMap_image_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)

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_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {s : Set α} {t : Set β} {f : γ → α} {g : δ → β} : (f ⁻¹' s) ×ˢ (g ⁻¹' t) = (fun (p : γ × δ) => (f p.1, g p.2)) ⁻¹' s ×ˢ t

theorem Set.prod_preimage_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {t : Set β} {f : γ → α} : (f ⁻¹' s) ×ˢ t = (fun (p : γ × β) => (f p.1, p.2)) ⁻¹' s ×ˢ t

theorem Set.prod_preimage_right {α : Type u_1} {β : Type u_2} {δ : Type u_4} {s : Set α} {t : Set β} {g : δ → β} : s ×ˢ (g ⁻¹' t) = (fun (p : α × δ) => (p.1, g p.2)) ⁻¹' s ×ˢ 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 ×ˢ t = (f ⁻¹' s) ×ˢ (g ⁻¹' t)

theorem Set.mk_preimage_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} {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_1} {β : Type u_2} {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) : Prod.mk a ⁻¹' s ×ˢ t = t

@[simp]

theorem Set.mk_preimage_prod_left_eq_empty {α : Type u_1} {β : Type u_2} {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) : Prod.mk a ⁻¹' s ×ˢ t = ∅

theorem Set.mk_preimage_prod_left_eq_if {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {b : β} [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 : α} [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_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {t : Set β} {b : β} [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_2} {δ : Type u_4} {s : Set α} {t : Set β} {a : α} [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.mapsTo_swap_prod {α : Type u_1} {β : Type u_2} (s : Set α) (t : Set β) : MapsTo Prod.swap (s ×ˢ t) (t ×ˢ s)

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) = (fun (p : α × β) => (m₁ p.1, m₂ p.2)) '' s ×ˢ t

theorem Set.prod_range_range_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {m₁ : α → γ} {m₂ : β → δ} : range m₁ ×ˢ range m₂ = range fun (p : α × β) => (m₁ p.1, m₂ p.2)

@[simp]

theorem Set.range_prodMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {m₁ : α → γ} {m₂ : β → δ} : range (Prod.map m₁ m₂) = range m₁ ×ˢ range m₂

@[deprecated Set.range_prodMap (since := "2025-04-10")]

theorem Set.range_prod_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {m₁ : α → γ} {m₂ : β → δ} : range (Prod.map m₁ m₂) = range m₁ ×ˢ range m₂

Alias of Set.range_prodMap.

theorem Set.prod_range_univ_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m₁ : α → γ} : range m₁ ×ˢ univ = range fun (p : α × β) => (m₁ p.1, p.2)

theorem Set.prod_univ_range_eq {α : Type u_1} {β : Type u_2} {δ : Type u_4} {m₂ : β → δ} : univ ×ˢ range m₂ = range fun (p : α × β) => (p.1, m₂ p.2)

theorem Set.range_pair_subset {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β) (g : α → γ) : (range fun (x : α) => (f x, g x)) ⊆ range f ×ˢ range g

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

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

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

@[simp]

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

@[simp]

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_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

theorem Set.image_prodMk_subset_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : α → γ} {s : Set α} : (fun (x : α) => (f x, g x)) '' s ⊆ (f '' s) ×ˢ (g '' s)

theorem Set.image_prodMk_subset_prod_left {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {b : β} (hb : b ∈ t) : (fun (a : α) => (a, b)) '' s ⊆ s ×ˢ t

theorem Set.image_prodMk_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_1} {β : Type u_2} (s : Set β) {t : Set α} (ht : t.Nonempty) : Prod.fst '' s ×ˢ t = s

theorem Set.mapsTo_fst_prod {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} : MapsTo 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 : s.Nonempty) (t : Set β) : Prod.snd '' s ×ˢ t = t

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

theorem Set.mapsTo_snd_prod {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} : MapsTo Prod.snd (s ×ˢ t) t

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

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.

theorem Set.prod_subset_prod_iff' {α : Type u_1} {β : Type u_2} {s s₁ : Set α} {t t₁ : Set β} (h : (s ×ˢ t).Nonempty) : s ×ˢ t ⊆ s₁ ×ˢ t₁ ↔ s ⊆ s₁ ∧ t ⊆ t₁

theorem Set.prod_subset_prod_iff_left {α : Type u_1} {β : Type u_2} {s s₁ : Set α} {t : Set β} (h : t.Nonempty) : s ×ˢ t ⊆ s₁ ×ˢ t ↔ s ⊆ s₁

theorem Set.prod_subset_prod_iff_right {α : Type u_1} {β : Type u_2} {s : Set α} {t t₁ : Set β} (h : s.Nonempty) : s ×ˢ t ⊆ s ×ˢ t₁ ↔ t ⊆ t₁

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₁

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

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

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

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 fun (x : α) => f x ×ˢ g x

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 fun (x : α) => f x ×ˢ g x

theorem MonotoneOn.set_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} [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 α} [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 fun x ↦ (x, x).

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

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

Equations

• Set.decidableMemDiagonal x = h x.1 x.2

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

@[simp]

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

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

@[simp]

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

@[simp]

theorem Set.diag_preimage_prod {α : Type u_1} (s 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 = diagonal α ∩ s ×ˢ s

theorem Set.diagonal_eq_univ_iff {α : Type u_1} : diagonal α = univ ↔ Subsingleton α

theorem Set.diagonal_eq_univ {α : Type u_1} [Subsingleton α] : diagonal α = univ

theorem Set.range_const_eq_diagonal {α : Type u_1} {β : Type u_2} [hβ : Nonempty β] : range (Function.const α) = {f : α → β | ∀ (x y : α), f x = f y}

A function is Function.const α a for some a if and only if ∀ x y, f x = f y.

@[reducible, inline]

abbrev Function.Pullback {X : Type u_1} {Y : Sort u_2} {Z : Type u_3} (f : X → Y) (g : Z → Y) : Type (max 0 u_3 u_1)

The fiber product $X \times_Y Z$.

Equations

• Function.Pullback f g = { p : X × Z // f p.1 = g p.2 }

@[reducible, inline]

abbrev Function.PullbackSelf {X : Type u_1} {Y : Sort u_2} (f : X → Y) : Type u_1

The fiber product $X \times_Y X$.

Equations

• Function.PullbackSelf f = Function.Pullback f f

def Function.Pullback.fst {X : Type u_1} {Y : Sort u_2} {Z : Type u_3} {f : X → Y} {g : Z → Y} (p : Pullback f g) : X

The projection from the fiber product to the first factor.

Equations

• p.fst = (↑p).1

def Function.Pullback.snd {X : Type u_1} {Y : Sort u_2} {Z : Type u_3} {f : X → Y} {g : Z → Y} (p : Pullback f g) : Z

The projection from the fiber product to the second factor.

Equations

• p.snd = (↑p).2

theorem Function.pullback_comm_sq {X : Type u_2} {Y : Sort u_3} {Z : Type u_1} (f : X → Y) (g : Z → Y) : f ∘ Pullback.fst = g ∘ Pullback.snd

def toPullbackDiag {X : Type u_1} {Y : Sort u_2} (f : X → Y) (x : X) : Function.Pullback f f

The diagonal map $\Delta: X \to X \times_Y X$.

Equations

• toPullbackDiag f x = ⟨(x, x), ⋯⟩

@[simp]

theorem toPullbackDiag_coe {X : Type u_1} {Y : Sort u_2} (f : X → Y) (x : X) : ↑(toPullbackDiag f x) = (x, x)

def Function.pullbackDiagonal {X : Type u_1} {Y : Sort u_2} (f : X → Y) : Set (Pullback f f)

The diagonal $\Delta(X) \subseteq X \times_Y X$.

Equations

• Function.pullbackDiagonal f = {p : Function.Pullback f f | p.fst = p.snd}

def Function.mapPullback {X₁ : Type u_1} {X₂ : Type u_2} {Y₁ : Sort u_3} {Y₂ : Sort u_4} {Z₁ : Type u_5} {Z₂ : Type u_6} {f₁ : X₁ → Y₁} {g₁ : Z₁ → Y₁} {f₂ : X₂ → Y₂} {g₂ : Z₂ → Y₂} (mapX : X₁ → X₂) (mapY : Y₁ → Y₂) (mapZ : Z₁ → Z₂) (commX : f₂ ∘ mapX = mapY ∘ f₁) (commZ : g₂ ∘ mapZ = mapY ∘ g₁) (p : Pullback f₁ g₁) : Pullback f₂ g₂

Three functions between the three pairs of spaces $X_i, Y_i, Z_i$ that are compatible induce a function $X_1 \times_{Y_1} Z_1 \to X_2 \times_{Y_2} Z_2$.

Equations

• Function.mapPullback mapX mapY mapZ commX commZ p = ⟨(mapX p.fst, mapZ p.snd), ⋯⟩

def Function.PullbackSelf.map_fst {X : Type u_1} {Y : Sort u_2} {Z : Type u_3} {f : X → Y} {g : Z → Y} : PullbackSelf Pullback.snd → PullbackSelf f

The projection $(X \times_Y Z) \times_Z (X \times_Y Z) \to X \times_Y X$.

Equations

• Function.PullbackSelf.map_fst = Function.mapPullback Function.Pullback.fst g Function.Pullback.fst ⋯ ⋯

def Function.PullbackSelf.map_snd {X : Type u_1} {Y : Sort u_2} {Z : Type u_3} {f : X → Y} {g : Z → Y} : PullbackSelf Pullback.fst → PullbackSelf g

The projection $(X \times_Y Z) \times_X (X \times_Y Z) \to Z \times_Y Z$.

Equations

• Function.PullbackSelf.map_snd = Function.mapPullback Function.Pullback.snd f Function.Pullback.snd ⋯ ⋯

theorem preimage_map_fst_pullbackDiagonal {X : Type u_2} {Y : Sort u_3} {Z : Type u_1} {f : X → Y} {g : Z → Y} : Function.PullbackSelf.map_fst ⁻¹' Function.pullbackDiagonal f = Function.pullbackDiagonal Function.Pullback.snd

theorem Function.Injective.preimage_pullbackDiagonal {X : Type u_2} {Y : Sort u_3} {Z : Type u_1} {f : X → Y} {g : Z → X} (inj : Injective g) : mapPullback g id g ⋯ ⋯ ⁻¹' pullbackDiagonal f = pullbackDiagonal (f ∘ g)

theorem image_toPullbackDiag {X : Type u_1} {Y : Sort u_2} (f : X → Y) (s : Set X) : toPullbackDiag f '' s = Function.pullbackDiagonal f ∩ Subtype.val ⁻¹' s ×ˢ s

theorem range_toPullbackDiag {X : Type u_1} {Y : Sort u_2} (f : X → Y) : Set.range (toPullbackDiag f) = Function.pullbackDiagonal f

theorem injective_toPullbackDiag {X : Type u_1} {Y : Sort u_2} (f : X → Y) : Function.Injective (toPullbackDiag f)

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

@[simp]

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

@[simp]

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

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

Alias of the reverse direction of Set.offDiag_nonempty.

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

Alias of the reverse direction of Set.offDiag_nonempty.

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

Cartesian set-indexed product of sets

@[simp]

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

theorem Set.subsingleton_univ_pi {ι : Type u_1} {α : ι → Type u_2} {t : (i : ι) → Set (α i)} (ht : ∀ (i : ι), (t i).Subsingleton) : (univ.pi t).Subsingleton

@[simp]

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

@[simp]

theorem Set.pi_univ_ite {ι : Type u_1} {α : ι → Type u_2} (s : Set ι) [DecidablePred fun (x : ι) => x ∈ s] (t : (i : ι) → Set (α i)) : (univ.pi fun (i : ι) => if i ∈ s then t i else univ) = s.pi t

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

theorem Set.pi_mono {ι : Type u_1} {α : ι → Type u_2} {s : Set ι} {t₁ t₂ : (i : ι) → Set (α i)} (h : ∀ i ∈ s, t₁ 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 fun (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 ∈ 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 = ∅) : univ.pi t = ∅

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

theorem Set.univ_pi_nonempty_iff {ι : Type u_1} {α : ι → Type u_2} {t : (i : ι) → Set (α i)} : (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 : ι), IsEmpty (α i) ∨ i ∈ s ∧ t i = ∅

@[simp]

theorem Set.univ_pi_eq_empty_iff {ι : Type u_1} {α : ι → Type u_2} {t : (i : ι) → Set (α i)} : univ.pi t = ∅ ↔ ∃ (i : ι), t i = ∅

@[simp]

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

@[simp]

theorem Set.disjoint_univ_pi {ι : Type u_1} {α : ι → Type u_2} {t₁ t₂ : (i : ι) → Set (α i)} : Disjoint (univ.pi t₁) (univ.pi t₂) ↔ ∃ (i : ι), Disjoint (t₁ i) (t₂ i)

theorem Set.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₂)

theorem Set.uniqueElim_preimage {ι : Type u_1} {α : ι → Type u_2} [Unique ι] (t : (i : ι) → Set (α i)) : uniqueElim ⁻¹' univ.pi t = t default

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 ∈ s, t i = ∅

@[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 ∈ s, Disjoint (t₁ i) (t₂ 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.univ_pi_singleton {ι : Type u_1} {α : ι → Type u_2} (f : (i : ι) → α i) : (univ.pi fun (i : ι) => {f i}) = {f}

theorem Set.preimage_pi {ι : Type u_1} {α : ι → Type u_2} {β : ι → Type u_3} (s : Set ι) (t : (i : ι) → Set (β i)) (f : (i : ι) → α i → β i) : (fun (g : (i : ι) → α i) (i : ι) => f i (g i)) ⁻¹' s.pi t = s.pi fun (i : ι) => f i ⁻¹' t i

theorem Set.pi_if {ι : Type u_1} {α : ι → Type u_2} {p : ι → Prop} [h : DecidablePred p] (s : Set ι) (t₁ t₂ : (i : ι) → Set (α i)) : (s.pi fun (i : ι) => if p i then t₁ i else t₂ i) = {i : ι | i ∈ s ∧ p i}.pi t₁ ∩ {i : ι | 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

theorem Set.union_pi_inter {ι : Type u_1} {α : ι → Type u_2} {s₁ s₂ : Set ι} {t₁ t₂ : (i : ι) → Set (α i)} (ht₁ : ∀ i ∉ s₁, t₁ i = univ) (ht₂ : ∀ i ∉ s₂, t₂ i = univ) : ((s₁ ∪ s₂).pi fun (i : ι) => t₁ i ∩ t₂ i) = 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 = univ.pi t

theorem Set.pi_update_of_notMem {ι : Type u_1} {α : ι → Type u_2} {β : ι → Type u_3} {s : Set ι} {i : ι} [DecidableEq ι] (hi : i ∉ s) (f : (j : ι) → α j) (a : α i) (t : (j : ι) → α j → Set (β j)) : (s.pi fun (j : ι) => t j (Function.update f i a j)) = s.pi fun (j : ι) => t j (f j)

@[deprecated Set.pi_update_of_notMem (since := "2025-05-23")]

theorem Set.pi_update_of_not_mem {ι : Type u_1} {α : ι → Type u_2} {β : ι → Type u_3} {s : Set ι} {i : ι} [DecidableEq ι] (hi : i ∉ s) (f : (j : ι) → α j) (a : α i) (t : (j : ι) → α j → Set (β j)) : (s.pi fun (j : ι) => t j (Function.update f i a j)) = s.pi fun (j : ι) => t j (f j)

Alias of Set.pi_update_of_notMem.

theorem Set.pi_update_of_mem {ι : Type u_1} {α : ι → Type u_2} {β : ι → Type u_3} {s : Set ι} {i : ι} [DecidableEq ι] (hi : i ∈ s) (f : (j : ι) → α j) (a : α i) (t : (j : ι) → α j → Set (β j)) : (s.pi fun (j : ι) => t j (Function.update f i a j)) = {x : (i : ι) → β i | x i ∈ t i a} ∩ (s \ {i}).pi fun (j : ι) => t j (f j)

theorem Set.univ_pi_update {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] {β : ι → Type u_4} (i : ι) (f : (j : ι) → α j) (a : α i) (t : (j : ι) → α j → Set (β j)) : (univ.pi fun (j : ι) => t j (Function.update f i a j)) = {x : (i : ι) → β i | x i ∈ t i a} ∩ {i}ᶜ.pi fun (j : ι) => t j (f j)

theorem Set.univ_pi_update_univ {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] (i : ι) (s : Set (α i)) : univ.pi (Function.update (fun (j : ι) => 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) : Function.eval i '' s.pi t ⊆ t i

theorem Set.eval_image_univ_pi_subset {ι : Type u_1} {α : ι → Type u_2} {t : (i : ι) → Set (α i)} {i : ι} : Function.eval i '' univ.pi t ⊆ t i

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

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

theorem Set.eval_image_pi_of_notMem {ι : Type u_1} {α : ι → Type u_2} {s : Set ι} {t : (i : ι) → Set (α i)} {i : ι} [Decidable (s.pi t).Nonempty] (hi : i ∉ s) : Function.eval i '' s.pi t = if (s.pi t).Nonempty then univ else ∅

@[deprecated Set.eval_image_pi_of_notMem (since := "2025-05-23")]

theorem Set.eval_image_pi_of_not_mem {ι : Type u_1} {α : ι → Type u_2} {s : Set ι} {t : (i : ι) → Set (α i)} {i : ι} [Decidable (s.pi t).Nonempty] (hi : i ∉ s) : Function.eval i '' s.pi t = if (s.pi t).Nonempty then univ else ∅

Alias of Set.eval_image_pi_of_notMem.

@[simp]

theorem Set.eval_image_univ_pi {ι : Type u_1} {α : ι → Type u_2} {t : (i : ι) → Set (α i)} {i : ι} (ht : (univ.pi t).Nonempty) : (fun (f : (i : ι) → α i) => f i) '' univ.pi t = t i

theorem Set.piMap_mapsTo_pi {ι : Type u_1} {α : ι → Type u_2} {β : ι → Type u_3} {I : Set ι} {f : (i : ι) → α i → β i} {s : (i : ι) → Set (α i)} {t : (i : ι) → Set (β i)} (h : ∀ i ∈ I, MapsTo (f i) (s i) (t i)) : MapsTo (Pi.map f) (I.pi s) (I.pi t)

theorem Set.piMap_image_pi_subset {ι : Type u_1} {α : ι → Type u_2} {β : ι → Type u_3} {s : Set ι} {f : (i : ι) → α i → β i} (t : (i : ι) → Set (α i)) : Pi.map f '' s.pi t ⊆ s.pi fun (i : ι) => f i '' t i

theorem Set.piMap_image_pi {ι : Type u_1} {α : ι → Type u_2} {β : ι → Type u_3} {s : Set ι} {f : (i : ι) → α i → β i} (hf : ∀ i ∉ s, Function.Surjective (f i)) (t : (i : ι) → Set (α i)) : Pi.map f '' s.pi t = s.pi fun (i : ι) => f i '' t i

theorem Set.piMap_image_univ_pi {ι : Type u_1} {α : ι → Type u_2} {β : ι → Type u_3} (f : (i : ι) → α i → β i) (t : (i : ι) → Set (α i)) : Pi.map f '' univ.pi t = univ.pi fun (i : ι) => f i '' t i

@[simp]

theorem Set.range_piMap {ι : Type u_1} {α : ι → Type u_2} {β : ι → Type u_3} (f : (i : ι) → α i → β i) : range (Pi.map f) = univ.pi fun (i : ι) => range (f i)

theorem Set.subset_pi_iff {ι : Type u_1} {α : ι → Type u_2} {s : Set ι} {t : (i : ι) → Set (α i)} {s' : Set ((i : ι) → α i)} : s' ⊆ s.pi t ↔ ∀ i ∈ s, s' ⊆ (fun (x : (i : ι) → α i) => x i) ⁻¹' t i

theorem Set.update_mem_pi_iff {ι : Type u_1} {α : ι → Type u_2} {s : Set ι} {t : (i : ι) → Set (α i)} [DecidableEq ι] {a : (i : ι) → α i} {i : ι} {b : α i} : Function.update a i b ∈ s.pi t ↔ a ∈ (s \ {i}).pi t ∧ (i ∈ s → b ∈ t i)

theorem Set.update_mem_pi_iff_of_mem {ι : Type u_1} {α : ι → Type u_2} {s : Set ι} {t : (i : ι) → Set (α i)} [DecidableEq ι] {a : (i : ι) → α i} {i : ι} {b : α i} (ha : a ∈ s.pi t) : Function.update a i b ∈ s.pi t ↔ i ∈ s → b ∈ t i

theorem Set.univ_pi_eq_singleton_iff {ι : Type u_1} {α : ι → Type u_2} {t : (i : ι) → Set (α i)} {a : (i : ι) → α i} : univ.pi t = {a} ↔ ∀ (i : ι), t i = {a i}

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

theorem Set.univ_pi_subset_univ_pi_iff {ι : Type u_1} {α : ι → Type u_2} {t₁ t₂ : (i : ι) → Set (α i)} : univ.pi t₁ ⊆ univ.pi t₂ ↔ (∀ (i : ι), t₁ i ⊆ t₂ i) ∨ ∃ (i : ι), t₁ i = ∅

theorem Set.eval_preimage {ι : Type u_1} {α : ι → Type u_2} {i : ι} [DecidableEq ι] {s : Set (α i)} : Function.eval i ⁻¹' s = univ.pi (Function.update (fun (x : ι) => univ) i s)

theorem Set.eval_preimage' {ι : Type u_1} {α : ι → Type u_2} {i : ι} [DecidableEq ι] {s : Set (α i)} : Function.eval i ⁻¹' s = {i}.pi (Function.update (fun (x : ι) => univ) i s)

theorem Set.update_preimage_pi {ι : Type u_1} {α : ι → Type u_2} {s : Set ι} {t : (i : ι) → Set (α i)} {i : ι} [DecidableEq ι] {f : (i : ι) → α i} (hi : i ∈ s) (hf : ∀ j ∈ s, j ≠ i → f j ∈ t j) : Function.update f i ⁻¹' s.pi t = t i

theorem Set.update_image {ι : Type u_1} {β : ι → Type u_3} [DecidableEq ι] (x : (i : ι) → β i) (i : ι) (s : Set (β i)) : Function.update x i '' s = univ.pi (Function.update (fun (j : ι) => {x j}) i s)

theorem Set.update_preimage_univ_pi {ι : Type u_1} {α : ι → Type u_2} {t : (i : ι) → Set (α i)} {i : ι} [DecidableEq ι] {f : (i : ι) → α i} (hf : ∀ (j : ι), j ≠ i → f j ∈ t j) : Function.update f i ⁻¹' univ.pi t = t i

theorem Set.subset_pi_eval_image {ι : Type u_1} {α : ι → Type u_2} (s : Set ι) (u : Set ((i : ι) → α i)) : u ⊆ s.pi fun (i : ι) => Function.eval i '' u

theorem Set.univ_pi_ite {ι : Type u_1} {α : ι → Type u_2} (s : Set ι) [DecidablePred fun (x : ι) => x ∈ s] (t : (i : ι) → Set (α i)) : (univ.pi fun (i : ι) => if i ∈ s then t i else univ) = s.pi t

theorem Set.uncurry_preimage_prod_pi {ι : Type u_1} {κ : Type u_4} {α : Type u_5} (s : Set ι) (t : Set κ) (u : ι × κ → Set α) : Function.uncurry ⁻¹' (s ×ˢ t).pi u = s.pi fun (i : ι) => t.pi fun (j : κ) => u (i, j)

theorem Equiv.piCongrLeft_symm_preimage_pi {ι : Type u_1} {ι' : Type u_2} {α : ι → Type u_3} (f : ι' ≃ ι) (s : Set ι') (t : (i : ι) → Set (α i)) : (⇑(piCongrLeft α f).symm ⁻¹' s.pi fun (i' : ι') => t (f i')) = (⇑f '' s).pi t

theorem Equiv.piCongrLeft_symm_preimage_univ_pi {ι : Type u_1} {ι' : Type u_2} {α : ι → Type u_3} (f : ι' ≃ ι) (t : (i : ι) → Set (α i)) : (⇑(piCongrLeft α f).symm ⁻¹' Set.univ.pi fun (i' : ι') => t (f i')) = Set.univ.pi t

theorem Equiv.piCongrLeft_preimage_pi {ι : Type u_1} {ι' : Type u_2} {α : ι → Type u_3} (f : ι' ≃ ι) (s : Set ι') (t : (i : ι) → Set (α i)) : ⇑(piCongrLeft α f) ⁻¹' (⇑f '' s).pi t = s.pi fun (i : ι') => t (f i)

theorem Equiv.piCongrLeft_preimage_univ_pi {ι : Type u_1} {ι' : Type u_2} {α : ι → Type u_3} (f : ι' ≃ ι) (t : (i : ι) → Set (α i)) : ⇑(piCongrLeft α f) ⁻¹' Set.univ.pi t = Set.univ.pi fun (i : ι') => t (f i)

theorem Equiv.sumPiEquivProdPi_symm_preimage_univ_pi {ι : Type u_1} {ι' : Type u_2} (π : ι ⊕ ι' → Type u_4) (t : (i : ι ⊕ ι') → Set (π i)) : ⇑(sumPiEquivProdPi π).symm ⁻¹' Set.univ.pi t = (Set.univ.pi fun (i : ι) => t (Sum.inl i)) ×ˢ Set.univ.pi fun (i : ι') => t (Sum.inr i)

@[simp]

theorem Set.mem_graphOn {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} {x : α × β} : x ∈ graphOn f s ↔ x.1 ∈ s ∧ f x.1 = x.2

@[simp]

theorem Set.graphOn_empty {α : Type u_1} {β : Type u_2} (f : α → β) : graphOn f ∅ = ∅

@[simp]

theorem Set.graphOn_eq_empty {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} : graphOn f s = ∅ ↔ s = ∅

@[simp]

theorem Set.graphOn_nonempty {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} : (graphOn f s).Nonempty ↔ s.Nonempty

theorem Set.Nonempty.graphOn {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} : s.Nonempty → (graphOn f s).Nonempty

Alias of the reverse direction of Set.graphOn_nonempty.

@[simp]

theorem Set.graphOn_union {α : Type u_1} {β : Type u_2} (f : α → β) (s t : Set α) : graphOn f (s ∪ t) = graphOn f s ∪ graphOn f t

@[simp]

theorem Set.graphOn_singleton {α : Type u_1} {β : Type u_2} (f : α → β) (x : α) : graphOn f {x} = {(x, f x)}

@[simp]

theorem Set.graphOn_insert {α : Type u_1} {β : Type u_2} (f : α → β) (x : α) (s : Set α) : graphOn f (insert x s) = insert (x, f x) (graphOn f s)

@[simp]

theorem Set.image_fst_graphOn {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α) : Prod.fst '' graphOn f s = s

@[simp]

theorem Set.image_snd_graphOn {α : Type u_1} {β : Type u_2} {s : Set α} (f : α → β) : Prod.snd '' graphOn f s = f '' s

theorem Set.fst_injOn_graph {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} : InjOn Prod.fst (graphOn f s)

theorem Set.graphOn_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (s : Set α) (f : α → β) (g : β → γ) : graphOn (g ∘ f) s = (fun (x : α × β) => (x.1, g x.2)) '' graphOn f s

theorem Set.graphOn_univ_eq_range {α : Type u_1} {β : Type u_2} {f : α → β} : graphOn f univ = range fun (x : α) => (x, f x)

@[simp]

theorem Set.graphOn_inj {α : Type u_1} {β : Type u_2} {s : Set α} {f g : α → β} : graphOn f s = graphOn g s ↔ EqOn f g s

theorem Set.graphOn_prod_graphOn {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (s : Set α) (t : Set β) (f : α → γ) (g : β → δ) : graphOn f s ×ˢ graphOn g t = ⇑(Equiv.prodProdProdComm α γ β δ) ⁻¹' graphOn (Prod.map f g) (s ×ˢ t)

theorem Set.graphOn_prod_prodMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (s : Set α) (t : Set β) (f : α → γ) (g : β → δ) : graphOn (Prod.map f g) (s ×ˢ t) = ⇑(Equiv.prodProdProdComm α β γ δ) ⁻¹' graphOn f s ×ˢ graphOn g t

Vertical line test

theorem Set.exists_range_eq_graphOn_univ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β × γ} (hf₁ : Function.Surjective (Prod.fst ∘ f)) (hf : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2) : ∃ (f' : β → γ), range f = graphOn f' univ

Vertical line test for functions.

Let f : α → β × γ be a function to a product. Assume that f is surjective on the first factor and that the image of f intersects every "vertical line" {(b, c) | c : γ} at most once. Then the image of f is the graph of some monoid homomorphism f' : β → γ.

theorem Set.exists_equiv_range_eq_graphOn_univ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β × γ} (hf₁ : Function.Surjective (Prod.fst ∘ f)) (hf₂ : Function.Surjective (Prod.snd ∘ f)) (hf : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2) : ∃ (e : β ≃ γ), range f = graphOn (⇑e) univ

Line test for equivalences.

Let f : α → β × γ be a homomorphism to a product of monoids. Assume that f is surjective on both factors and that the image of f intersects every "vertical line" {(b, c) | c : γ} and every "horizontal line" {(b, c) | b : β} at most once. Then the image of f is the graph of some equivalence f' : β ≃ γ.

theorem Set.exists_eq_mgraphOn_univ {β : Type u_2} {γ : Type u_3} {s : Set (β × γ)} (hs₁ : Function.Bijective (Prod.fst ∘ Subtype.val)) : ∃ (f : β → γ), s = graphOn f univ

Vertical line test for functions.

Let s : Set (β × γ) be a set in a product. Assume that s maps bijectively to the first factor. Then s is the graph of some function f : β → γ.