Mathlib.Data.Set.Prod

Set.Subsingleton.prod theorem

(hs : s.Subsingleton) (ht : t.Subsingleton) : (s ×ˢ t).Subsingleton

Full source

theorem Subsingleton.prod (hs : s.Subsingleton) (ht : t.Subsingleton) :
    (s ×ˢ t).Subsingleton := fun _x hx _y hy ↦
  Prod.ext (hs hx.1 hy.1) (ht hx.2 hy.2)

Cartesian Product of Subsingleton Sets is Subsingleton

Informal description

If $s$ is a subsingleton set in type $\alpha$ and $t$ is a subsingleton set in type $\beta$, then their Cartesian product $s \timesˢ t$ is also a subsingleton set in $\alpha \times \beta$.

Set.decidableMemProd instance

[DecidablePred (· ∈ s)] [DecidablePred (· ∈ t)] : DecidablePred (· ∈ s ×ˢ t)

Full source

noncomputable instance decidableMemProd [DecidablePred (· ∈ s)] [DecidablePred (· ∈ t)] :
    DecidablePred (· ∈ s ×ˢ t) := fun x => inferInstanceAs (Decidable (x.1 ∈ sx.1 ∈ s ∧ x.2 ∈ t))

Decidability of Membership in Cartesian Product of Sets

Informal description

For any sets $s \subseteq \alpha$ and $t \subseteq \beta$ with decidable membership predicates, the membership in their Cartesian product $s \timesˢ t$ is also decidable. That is, for any pair $(a, b) \in \alpha \times \beta$, it is decidable whether $a \in s$ and $b \in t$.

Set.prod_mono theorem

(hs : s₁ ⊆ s₂) (ht : t₁ ⊆ t₂) : s₁ ×ˢ t₁ ⊆ s₂ ×ˢ t₂

Full source

@[gcongr]
theorem prod_mono (hs : s₁ ⊆ s₂) (ht : t₁ ⊆ t₂) : s₁ ×ˢ t₁ ⊆ s₂ ×ˢ t₂ :=
  fun _ ⟨h₁, h₂⟩ => ⟨hs h₁, ht h₂⟩

Monotonicity of Cartesian Product with Respect to Subset Inclusion

Informal description

For any sets $s_1, s_2 \subseteq \alpha$ and $t_1, t_2 \subseteq \beta$, if $s_1 \subseteq s_2$ and $t_1 \subseteq t_2$, then the Cartesian product $s_1 \times t_1$ is a subset of $s_2 \times t_2$.

Set.prod_mono_left theorem

(hs : s₁ ⊆ s₂) : s₁ ×ˢ t ⊆ s₂ ×ˢ t

Full source

@[gcongr]
theorem prod_mono_left (hs : s₁ ⊆ s₂) : s₁ ×ˢ t ⊆ s₂ ×ˢ t :=
  prod_mono hs Subset.rfl

Left Monotonicity of Cartesian Product with Respect to Subset Inclusion

Informal description

For any sets $s_1, s_2 \subseteq \alpha$ and $t \subseteq \beta$, if $s_1$ is a subset of $s_2$, then the Cartesian product $s_1 \times t$ is a subset of $s_2 \times t$.

Set.prod_mono_right theorem

(ht : t₁ ⊆ t₂) : s ×ˢ t₁ ⊆ s ×ˢ t₂

Full source

@[gcongr]
theorem prod_mono_right (ht : t₁ ⊆ t₂) : s ×ˢ t₁ ⊆ s ×ˢ t₂ :=
  prod_mono Subset.rfl ht

Right Monotonicity of Cartesian Product with Respect to Subset Inclusion

Informal description

For any sets $s \subseteq \alpha$ and $t_1, t_2 \subseteq \beta$, if $t_1 \subseteq t_2$, then the Cartesian product $s \times t_1$ is a subset of $s \times t_2$.

Set.prod_self_subset_prod_self theorem

: s₁ ×ˢ s₁ ⊆ s₂ ×ˢ s₂ ↔ s₁ ⊆ s₂

Full source

@[simp]
theorem prod_self_subset_prod_self : s₁ ×ˢ s₁ ⊆ s₂ ×ˢ s₂s₁ ×ˢ s₁ ⊆ s₂ ×ˢ s₂ ↔ s₁ ⊆ s₂ :=
  ⟨fun h _ hx => (h (mk_mem_prod hx hx)).1, fun h _ hx => ⟨h hx.1, h hx.2⟩⟩

Subset Relation of Cartesian Squares: $s_1 \times s_1 \subseteq s_2 \times s_2 \leftrightarrow s_1 \subseteq s_2$

Informal description

For any two sets $s_1$ and $s_2$ in a type $\alpha$, the Cartesian product $s_1 \times s_1$ is a subset of $s_2 \times s_2$ if and only if $s_1$ is a subset of $s_2$.

Set.prod_self_ssubset_prod_self theorem

: s₁ ×ˢ s₁ ⊂ s₂ ×ˢ s₂ ↔ s₁ ⊂ s₂

Full source

@[simp]
theorem prod_self_ssubset_prod_self : s₁ ×ˢ s₁ ⊂ s₂ ×ˢ s₂s₁ ×ˢ s₁ ⊂ s₂ ×ˢ s₂ ↔ s₁ ⊂ s₂ :=
  and_congr prod_self_subset_prod_self <| not_congr prod_self_subset_prod_self

Strict Subset Relation of Cartesian Squares: $s_1 \times s_1 \subset s_2 \times s_2 \leftrightarrow s_1 \subset s_2$

Informal description

For any two sets $s_1$ and $s_2$ in a type $\alpha$, the Cartesian product $s_1 \times s_1$ is a strict subset of $s_2 \times s_2$ if and only if $s_1$ is a strict subset of $s_2$.

Set.prod_subset_iff theorem

{P : Set (α × β)} : s ×ˢ t ⊆ P ↔ ∀ x ∈ s, ∀ y ∈ t, (x, y) ∈ P

Full source

theorem prod_subset_iff {P : Set (α × β)} : s ×ˢ t ⊆ Ps ×ˢ t ⊆ P ↔ ∀ x ∈ s, ∀ y ∈ t, (x, y) ∈ P :=
  ⟨fun h _ hx _ hy => h (mk_mem_prod hx hy), fun h ⟨_, _⟩ hp => h _ hp.1 _ hp.2⟩

Subset Criterion for Cartesian Product: $s \times t \subseteq P \leftrightarrow \forall x \in s, \forall y \in t, (x,y) \in P$

Informal description

For any sets $s \subseteq \alpha$, $t \subseteq \beta$, and $P \subseteq \alpha \times \beta$, the Cartesian product $s \times t$ is a subset of $P$ if and only if for every $x \in s$ and every $y \in t$, the pair $(x, y)$ belongs to $P$.

Set.forall_prod_set theorem

{p : α × β → Prop} : (∀ x ∈ s ×ˢ t, p x) ↔ ∀ x ∈ s, ∀ y ∈ t, p (x, y)

Full source

theorem forall_prod_set {p : α × β → Prop} : (∀ x ∈ s ×ˢ t, p x) ↔ ∀ x ∈ s, ∀ y ∈ t, p (x, y) :=
  prod_subset_iff

Universal Quantification over Cartesian Product: $(\forall (x,y) \in s \times t, p(x,y)) \leftrightarrow (\forall x \in s, \forall y \in t, p(x,y))$

Informal description

For any predicate $p$ on the Cartesian product $\alpha \times \beta$, the statement $p(x, y)$ holds for all $(x, y) \in s \times t$ if and only if for every $x \in s$ and every $y \in t$, the predicate $p(x, y)$ holds.

Set.exists_prod_set theorem

{p : α × β → Prop} : (∃ x ∈ s ×ˢ t, p x) ↔ ∃ x ∈ s, ∃ y ∈ t, p (x, y)

Full source

theorem exists_prod_set {p : α × β → Prop} : (∃ x ∈ s ×ˢ t, p x) ↔ ∃ x ∈ s, ∃ y ∈ t, p (x, y) := by
  simp [and_assoc]

Existence in Cartesian Product of Sets

Informal description

For any predicate $p$ on $\alpha \times \beta$, there exists an element $(x, y)$ in the Cartesian product $s \times t$ satisfying $p(x, y)$ if and only if there exists $x \in s$ and $y \in t$ such that $p(x, y)$ holds.

Set.prod_empty theorem

: s ×ˢ (∅ : Set β) = ∅

Full source

@[simp]
theorem prod_empty : s ×ˢ (∅ : Set β) = ∅ := by
  ext
  exact iff_of_eq (and_false _)

Cartesian Product with Empty Set is Empty

Informal description

For any set $s$ in a type $\alpha$, the Cartesian product $s \times \emptyset$ is equal to the empty set, i.e., $s \times \emptyset = \emptyset$.

Set.empty_prod theorem

: (∅ : Set α) ×ˢ t = ∅

Full source

@[simp]
theorem empty_prod : (∅ : Set α) ×ˢ t = ∅ := by
  ext
  exact iff_of_eq (false_and _)

Empty Set Cartesian Product Property: $\emptyset \timesˢ t = \emptyset$

Informal description

The Cartesian product of the empty set (of type $\alpha$) with any set $t$ (of type $\beta$) is the empty set (of type $\alpha \times \beta$), i.e., $\emptyset \timesˢ t = \emptyset$.

Set.univ_prod_univ theorem

: @univ α ×ˢ @univ β = univ

Full source

@[simp, mfld_simps]
theorem univ_prod_univ : @univ α ×ˢ @univ β = univ := by
  ext
  exact iff_of_eq (true_and _)

Universal Set Product Identity: $\text{univ}_{\alpha} \timesˢ \text{univ}_{\beta} = \text{univ}_{\alpha \times \beta}$

Informal description

The Cartesian product of the universal set on $\alpha$ and the universal set on $\beta$ is equal to the universal set on $\alpha \times \beta$, i.e., $\text{univ}_{\alpha} \timesˢ \text{univ}_{\beta} = \text{univ}_{\alpha \times \beta}$.

Set.univ_prod theorem

{t : Set β} : (univ : Set α) ×ˢ t = Prod.snd ⁻¹' t

Full source

theorem univ_prod {t : Set β} : (univ : Set α) ×ˢ t = Prod.sndProd.snd ⁻¹' t := by simp [prod_eq]

Universal Set Product as Preimage of Second Projection

Informal description

For any set $t \subseteq \beta$, the Cartesian product of the universal set on $\alpha$ with $t$ is equal to the preimage of $t$ under the second projection map $\text{snd} : \alpha \times \beta \to \beta$, i.e., $\text{univ}_\alpha \timesˢ t = \text{snd}^{-1}(t)$.

Set.prod_univ theorem

{s : Set α} : s ×ˢ (univ : Set β) = Prod.fst ⁻¹' s

Full source

theorem prod_univ {s : Set α} : s ×ˢ (univ : Set β) = Prod.fstProd.fst ⁻¹' s := by simp [prod_eq]

Cartesian Product with Universal Set Equals Preimage of First Projection

Informal description

For any set $s \subseteq \alpha$, the Cartesian product $s \times \beta$ is equal to the preimage of $s$ under the first projection function $\pi_1 : \alpha \times \beta \to \alpha$, i.e., $s \times \beta = \pi_1^{-1}(s)$.

Set.prod_eq_univ theorem

[Nonempty α] [Nonempty β] : s ×ˢ t = univ ↔ s = univ ∧ t = univ

Full source

@[simp] lemma prod_eq_univ [Nonempty α] [Nonempty β] : s ×ˢ t = univ ↔ s = univ ∧ t = univ := by
  simp [eq_univ_iff_forall, forall_and]

Cartesian Product Equals Universal Set iff Both Factors Are Universal Sets

Informal description

Let $\alpha$ and $\beta$ be nonempty types, and let $s \subseteq \alpha$ and $t \subseteq \beta$ be sets. The Cartesian product $s \times t$ equals the universal set $\alpha \times \beta$ if and only if both $s = \alpha$ and $t = \beta$.

Set.singleton_prod theorem

: ({ a } : Set α) ×ˢ t = Prod.mk a '' t

Full source

theorem singleton_prod : ({a} : Set α) ×ˢ t = Prod.mkProd.mk a '' t := by
  ext ⟨x, y⟩
  simp [and_left_comm, eq_comm]

Cartesian Product of Singleton with Set Equals Image of Pairing Function

Informal description

For any element $a \in \alpha$ and any set $t \subseteq \beta$, the Cartesian product $\{a\} \times t$ is equal to the image of $t$ under the function $\lambda b, (a, b)$.

Set.prod_singleton theorem

: s ×ˢ ({ b } : Set β) = (fun a => (a, b)) '' s

Full source

theorem prod_singleton : s ×ˢ ({b} : Set β) = (fun a => (a, b)) '' s := by
  ext ⟨x, y⟩
  simp [and_left_comm, eq_comm]

Cartesian Product with Singleton Equals Image of Pairing Function

Informal description

For any set $s \subseteq \alpha$ and any singleton set $\{b\} \subseteq \beta$, the Cartesian product $s \times \{b\}$ is equal to the image of $s$ under the function $a \mapsto (a, b)$.

Set.singleton_prod_singleton theorem

: ({ a } : Set α) ×ˢ ({ b } : Set β) = {(a, b)}

Full source

@[simp]
theorem singleton_prod_singleton : ({a} : Set α) ×ˢ ({b} : Set β) = {(a, b)} := by ext ⟨c, d⟩; simp

Cartesian Product of Singletons is Singleton Pair: $\{a\} \times \{b\} = \{(a, b)\}$

Informal description

For any elements $a \in \alpha$ and $b \in \beta$, the Cartesian product of the singleton sets $\{a\}$ and $\{b\}$ is the singleton set $\{(a, b)\}$ in $\alpha \times \beta$.

Set.union_prod theorem

: (s₁ ∪ s₂) ×ˢ t = s₁ ×ˢ t ∪ s₂ ×ˢ t

Full source

@[simp]
theorem union_prod : (s₁ ∪ s₂) ×ˢ t = s₁ ×ˢ t ∪ s₂ ×ˢ t := by
  ext ⟨x, y⟩
  simp [or_and_right]

Distributivity of Cartesian Product over Union in the First Component

Informal description

For any sets $s_1, s_2 \subseteq \alpha$ and $t \subseteq \beta$, the Cartesian product of the union $s_1 \cup s_2$ with $t$ is equal to the union of the Cartesian products $s_1 \times t$ and $s_2 \times t$. In other words, $$(s_1 \cup s_2) \times t = (s_1 \times t) \cup (s_2 \times t).$$

Set.prod_union theorem

: s ×ˢ (t₁ ∪ t₂) = s ×ˢ t₁ ∪ s ×ˢ t₂

Full source

@[simp]
theorem prod_union : s ×ˢ (t₁ ∪ t₂) = s ×ˢ t₁ ∪ s ×ˢ t₂ := by
  ext ⟨x, y⟩
  simp [and_or_left]

Distributivity of Cartesian Product over Union: $s \times (t_1 \cup t_2) = (s \times t_1) \cup (s \times t_2)$

Informal description

For any sets $s \subseteq \alpha$, $t_1 \subseteq \beta$, and $t_2 \subseteq \beta$, the Cartesian product $s \times (t_1 \cup t_2)$ is equal to the union of the Cartesian products $(s \times t_1) \cup (s \times t_2)$.

Set.inter_prod theorem

: (s₁ ∩ s₂) ×ˢ t = s₁ ×ˢ t ∩ s₂ ×ˢ t

Full source

theorem inter_prod : (s₁ ∩ s₂) ×ˢ t = s₁ ×ˢ t ∩ s₂ ×ˢ t := by
  ext ⟨x, y⟩
  simp only [← and_and_right, mem_inter_iff, mem_prod]

Intersection Distributes Over Cartesian Product: $(s_1 \cap s_2) \timesˢ t = (s_1 \timesˢ t) \cap (s_2 \timesˢ t)$

Informal description

For any sets $s_1, s_2 \subseteq \alpha$ and $t \subseteq \beta$, the Cartesian product of the intersection $s_1 \cap s_2$ with $t$ is equal to the intersection of the Cartesian products $s_1 \timesˢ t$ and $s_2 \timesˢ t$. In symbols: $$(s_1 \cap s_2) \timesˢ t = (s_1 \timesˢ t) \cap (s_2 \timesˢ t).$$

Set.prod_inter theorem

: s ×ˢ (t₁ ∩ t₂) = s ×ˢ t₁ ∩ s ×ˢ t₂

Full source

theorem prod_inter : s ×ˢ (t₁ ∩ t₂) = s ×ˢ t₁ ∩ s ×ˢ t₂ := by
  ext ⟨x, y⟩
  simp only [← and_and_left, mem_inter_iff, mem_prod]

Cartesian Product Distributes over Intersection: $s \times (t_1 \cap t_2) = (s \times t_1) \cap (s \times t_2)$

Informal description

For any sets $s \subseteq \alpha$, $t_1 \subseteq \beta$, and $t_2 \subseteq \beta$, the Cartesian product of $s$ with the intersection of $t_1$ and $t_2$ is equal to the intersection of the Cartesian products $s \times t_1$ and $s \times t_2$. In symbols: $$ s \times (t_1 \cap t_2) = (s \times t_1) \cap (s \times t_2) $$

Set.prod_inter_prod theorem

: s₁ ×ˢ t₁ ∩ s₂ ×ˢ t₂ = (s₁ ∩ s₂) ×ˢ (t₁ ∩ t₂)

Full source

@[mfld_simps]
theorem prod_inter_prod : s₁ ×ˢ t₁ ∩ s₂ ×ˢ t₂ = (s₁ ∩ s₂) ×ˢ (t₁ ∩ t₂) := by
  ext ⟨x, y⟩
  simp [and_assoc, and_left_comm]

Intersection of Cartesian Products Equals Cartesian Product of Intersections

Informal description

For any sets $s_1, s_2 \subseteq \alpha$ and $t_1, t_2 \subseteq \beta$, the intersection of the Cartesian products $s_1 \times t_1$ and $s_2 \times t_2$ is equal to the Cartesian product of the intersections $(s_1 \cap s_2) \times (t_1 \cap t_2)$. In symbols: $$ (s_1 \times t_1) \cap (s_2 \times t_2) = (s_1 \cap s_2) \times (t_1 \cap t_2). $$

Set.compl_prod_eq_union theorem

{α β : Type*} (s : Set α) (t : Set β) : (s ×ˢ t)ᶜ = (sᶜ ×ˢ univ) ∪ (univ ×ˢ tᶜ)

Full source

lemma compl_prod_eq_union {α β : Type*} (s : Set α) (t : Set β) :
    (s ×ˢ t)ᶜ = (sᶜ ×ˢ univ) ∪ (univ ×ˢ tᶜ) := by
  ext p
  simp only [mem_compl_iff, mem_prod, not_and, mem_union, mem_univ, and_true, true_and]
  constructor <;> intro h
  · by_cases fst_in_s : p.fst ∈ s
    · exact Or.inr (h fst_in_s)
    · exact Or.inl fst_in_s
  · intro fst_in_s
    simpa only [fst_in_s, not_true, false_or] using h

Complement of Cartesian Product Decomposition

Informal description

For any sets $s \subseteq \alpha$ and $t \subseteq \beta$, the complement of their Cartesian product $s \timesˢ t$ is equal to the union of the Cartesian product of the complement of $s$ with the universal set $\alpha$ and the Cartesian product of the universal set $\beta$ with the complement of $t$. In symbols: $$(s \timesˢ t)^c = (s^c \times \beta) \cup (\alpha \times t^c).$$

Set.disjoint_prod theorem

: Disjoint (s₁ ×ˢ t₁) (s₂ ×ˢ t₂) ↔ Disjoint s₁ s₂ ∨ Disjoint t₁ t₂

Full source

@[simp]
theorem disjoint_prod : DisjointDisjoint (s₁ ×ˢ t₁) (s₂ ×ˢ t₂) ↔ Disjoint s₁ s₂ ∨ Disjoint t₁ t₂ := by
  simp_rw [disjoint_left, mem_prod, not_and_or, Prod.forall, and_imp, ← @forall_or_right α, ←
    @forall_or_left β, ← @forall_or_right (_ ∈ s₁), ← @forall_or_left (_ ∈ t₁)]

Disjointness of Cartesian Products is Equivalent to Disjointness of Components

Informal description

For any sets $s_1, s_2 \subseteq \alpha$ and $t_1, t_2 \subseteq \beta$, the Cartesian products $s_1 \times t_1$ and $s_2 \times t_2$ are disjoint if and only if either $s_1$ and $s_2$ are disjoint or $t_1$ and $t_2$ are disjoint. In symbols: $$ \text{Disjoint}(s_1 \times t_1, s_2 \times t_2) \leftrightarrow \text{Disjoint}(s_1, s_2) \lor \text{Disjoint}(t_1, t_2). $$

Set.Disjoint.set_prod_left theorem

(hs : Disjoint s₁ s₂) (t₁ t₂ : Set β) : Disjoint (s₁ ×ˢ t₁) (s₂ ×ˢ t₂)

Full source

theorem Disjoint.set_prod_left (hs : Disjoint s₁ s₂) (t₁ t₂ : Set β) :
    Disjoint (s₁ ×ˢ t₁) (s₂ ×ˢ t₂) :=
  disjoint_left.2 fun ⟨_a, _b⟩ ⟨ha₁, _⟩ ⟨ha₂, _⟩ => disjoint_left.1 hs ha₁ ha₂

Disjointness of Cartesian Products from Disjoint Factors

Informal description

For any sets $s_1, s_2 \subseteq \alpha$ that are disjoint, and any sets $t_1, t_2 \subseteq \beta$, the Cartesian products $s_1 \times t_1$ and $s_2 \times t_2$ are also disjoint.

Set.Disjoint.set_prod_right theorem

(ht : Disjoint t₁ t₂) (s₁ s₂ : Set α) : Disjoint (s₁ ×ˢ t₁) (s₂ ×ˢ t₂)

Full source

theorem Disjoint.set_prod_right (ht : Disjoint t₁ t₂) (s₁ s₂ : Set α) :
    Disjoint (s₁ ×ˢ t₁) (s₂ ×ˢ t₂) :=
  disjoint_left.2 fun ⟨_a, _b⟩ ⟨_, hb₁⟩ ⟨_, hb₂⟩ => disjoint_left.1 ht hb₁ hb₂

Disjointness of Cartesian Products When Second Components Are Disjoint

Informal description

For any two disjoint sets $t_1, t_2 \subseteq \beta$ and any two sets $s_1, s_2 \subseteq \alpha$, the Cartesian products $s_1 \times t_1$ and $s_2 \times t_2$ are disjoint in $\alpha \times \beta$.

Set.prodMap_image_prod theorem

(f : α → β) (g : γ → δ) (s : Set α) (t : Set γ) : (Prod.map f g) '' (s ×ˢ t) = (f '' s) ×ˢ (g '' t)

Full source

theorem prodMap_image_prod (f : α → β) (g : γ → δ) (s : Set α) (t : Set γ) :
    (Prod.map f g) '' (s ×ˢ t) = (f '' s) ×ˢ (g '' t) := by
  ext
  aesop

Image of Cartesian Product under Product Map Equals Product of Images

Informal description

For any sets $s \subseteq \alpha$ and $t \subseteq \gamma$, and any functions $f : \alpha \to \beta$ and $g : \gamma \to \delta$, the image of the Cartesian product $s \times t$ under the product map $(f, g)$ is equal to the Cartesian product of the images $f(s) \times g(t)$. In other words: $$(f \times g)(s \times t) = f(s) \times g(t)$$

Set.insert_prod theorem

: insert a s ×ˢ t = Prod.mk a '' t ∪ s ×ˢ t

Full source

theorem insert_prod : insert a s ×ˢ t = Prod.mkProd.mk a '' tProd.mk a '' t ∪ s ×ˢ t := by
  simp only [insert_eq, union_prod, singleton_prod]

Cartesian Product with Inserted Element Equals Union of Singleton Product and Original Product

Informal description

For any element $a \in \alpha$, any set $s \subseteq \alpha$, and any set $t \subseteq \beta$, the Cartesian product of the set $\{a\} \cup s$ with $t$ is equal to the union of the image of $t$ under the function $\lambda b, (a, b)$ and the Cartesian product $s \times t$. In other words: $$(\{a\} \cup s) \times t = \{(a, b) \mid b \in t\} \cup (s \times t).$$

Set.prod_insert theorem

: s ×ˢ insert b t = (fun a => (a, b)) '' s ∪ s ×ˢ t

Full source

theorem prod_insert : s ×ˢ insert b t = (fun a => (a, b)) '' s(fun a => (a, b)) '' s ∪ s ×ˢ t := by
  simp only [insert_eq, prod_union, prod_singleton]

Distributivity of Cartesian Product over Insertion: $s \times (t \cup \{b\}) = \{(a,b) \mid a \in s\} \cup (s \times t)$

Informal description

For any set $s \subseteq \alpha$ and any set $t \subseteq \beta$ containing an element $b$, the Cartesian product $s \times (t \cup \{b\})$ is equal to the union of the image of $s$ under the map $a \mapsto (a,b)$ and the Cartesian product $s \times t$. In other words: $$ s \times (t \cup \{b\}) = \{(a,b) \mid a \in s\} \cup (s \times t) $$

Set.prod_preimage_eq theorem

{f : γ → α} {g : δ → β} : (f ⁻¹' s) ×ˢ (g ⁻¹' t) = (fun p : γ × δ => (f p.1, g p.2)) ⁻¹' s ×ˢ t

Full source

theorem prod_preimage_eq {f : γ → α} {g : δ → β} :
    (f ⁻¹' s) ×ˢ (g ⁻¹' t) = (fun p : γ × δ => (f p.1, g p.2)) ⁻¹' s ×ˢ t :=
  rfl

Preimage of Cartesian Product under Component-wise Mapping

Informal description

For any functions $f : \gamma \to \alpha$ and $g : \delta \to \beta$, the Cartesian product of the preimages $f^{-1}(s) \times g^{-1}(t)$ is equal to the preimage of $s \times t$ under the function $(p : \gamma \times \delta) \mapsto (f(p_1), g(p_2))$.

Set.prod_preimage_left theorem

{f : γ → α} : (f ⁻¹' s) ×ˢ t = (fun p : γ × β => (f p.1, p.2)) ⁻¹' s ×ˢ t

Full source

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

Preimage of Cartesian Product under Left Projection

Informal description

For any function $f : \gamma \to \alpha$ and sets $s \subseteq \alpha$, $t \subseteq \beta$, the Cartesian product of the preimage $f^{-1}(s)$ with $t$ is equal to the preimage of $s \timesˢ t$ under the map $(p : \gamma \times \beta) \mapsto (f(p_1), p_2)$. In other words, $$ f^{-1}(s) \timesˢ t = \{(x, y) \in \gamma \times \beta \mid (f(x), y) \in s \timesˢ t\}. $$

Set.prod_preimage_right theorem

{g : δ → β} : s ×ˢ (g ⁻¹' t) = (fun p : α × δ => (p.1, g p.2)) ⁻¹' s ×ˢ t

Full source

theorem prod_preimage_right {g : δ → β} :
    s ×ˢ (g ⁻¹' t) = (fun p : α × δ => (p.1, g p.2)) ⁻¹' s ×ˢ t :=
  rfl

Preimage of Cartesian Product under Right Projection and Function Application

Informal description

For any sets $s \subseteq \alpha$ and $t \subseteq \beta$, and any function $g : \delta \to \beta$, the Cartesian product $s \timesˢ (g^{-1}(t))$ is equal to the preimage of $s \timesˢ t$ under the function $(p : \alpha \times \delta) \mapsto (p.1, g(p.2))$.

Set.preimage_prod_map_prod theorem

 (f : α → β) (g : γ → δ) (s : Set β) (t : Set δ) : Prod.map f g ⁻¹' s ×ˢ t = (f ⁻¹' s) ×ˢ (g ⁻¹' t)

Full source

theorem preimage_prod_map_prod (f : α → β) (g : γ → δ) (s : Set β) (t : Set δ) :
    Prod.mapProd.map f g ⁻¹' s ×ˢ t = (f ⁻¹' s) ×ˢ (g ⁻¹' t) :=
  rfl

Preimage of Product Set under Product Map

Informal description

For any functions $f : \alpha \to \beta$ and $g : \gamma \to \delta$, and any sets $s \subseteq \beta$ and $t \subseteq \delta$, the preimage of the product set $s \timesˢ t$ under the product map $\text{Prod.map}\, f\, g$ is equal to the product of the preimages of $s$ under $f$ and $t$ under $g$. In other words, $$(f \times g)^{-1}(s \times t) = f^{-1}(s) \times g^{-1}(t).$$

Set.mk_preimage_prod theorem

(f : γ → α) (g : γ → β) : (fun x => (f x, g x)) ⁻¹' s ×ˢ t = f ⁻¹' s ∩ g ⁻¹' t

Full source

theorem mk_preimage_prod (f : γ → α) (g : γ → β) :
    (fun x => (f x, g x)) ⁻¹' s ×ˢ t = f ⁻¹' sf ⁻¹' s ∩ g ⁻¹' t :=
  rfl

Preimage of Cartesian Product Under Pair Map Equals Intersection of Preimages

Informal description

For any functions $f : \gamma \to \alpha$ and $g : \gamma \to \beta$, and sets $s \subseteq \alpha$ and $t \subseteq \beta$, the preimage of the Cartesian product $s \timesˢ t$ under the map $x \mapsto (f(x), g(x))$ is equal to the intersection of the preimages $f^{-1}(s)$ and $g^{-1}(t)$. In other words: $$(x \mapsto (f(x), g(x)))^{-1}(s \times t) = f^{-1}(s) \cap g^{-1}(t)$$

Set.mk_preimage_prod_left theorem

(hb : b ∈ t) : (fun a => (a, b)) ⁻¹' s ×ˢ t = s

Full source

@[simp]
theorem mk_preimage_prod_left (hb : b ∈ t) : (fun a => (a, b)) ⁻¹' s ×ˢ t = s := by
  ext a
  simp [hb]

Preimage of Cartesian Product under Fixed Second Coordinate Function

Informal description

For any sets $s \subseteq \alpha$ and $t \subseteq \beta$, and any element $b \in t$, the preimage of the Cartesian product $s \timesˢ t$ under the function $a \mapsto (a, b)$ is equal to $s$.

Set.mk_preimage_prod_right theorem

(ha : a ∈ s) : Prod.mk a ⁻¹' s ×ˢ t = t

Full source

@[simp]
theorem mk_preimage_prod_right (ha : a ∈ s) : Prod.mkProd.mk a ⁻¹' s ×ˢ t = t := by
  ext b
  simp [ha]

Preimage of Cartesian Product under Right Projection when $a \in s$: $\{b \mid (a,b) \in s \times t\} = t$

Informal description

For any element $a$ in a set $s \subseteq \alpha$ and any set $t \subseteq \beta$, the preimage of the Cartesian product $s \timesˢ t$ under the function $\lambda b \mapsto (a, b)$ is equal to $t$. In other words, if $a \in s$, then $\{b \in \beta \mid (a, b) \in s \timesˢ t\} = t$.

Set.mk_preimage_prod_left_eq_empty theorem

(hb : b ∉ t) : (fun a => (a, b)) ⁻¹' s ×ˢ t = ∅

Full source

@[simp]
theorem mk_preimage_prod_left_eq_empty (hb : b ∉ t) : (fun a => (a, b)) ⁻¹' s ×ˢ t = ∅ := by
  ext a
  simp [hb]

Empty Preimage of Cartesian Product for Non-Member Element

Informal description

For any sets $s \subseteq \alpha$ and $t \subseteq \beta$, and any element $b \notin t$, the preimage of the Cartesian product $s \timesˢ t$ under the function $a \mapsto (a, b)$ is the empty set, i.e., $\{a \in \alpha \mid (a, b) \in s \timesˢ t\} = \emptyset$.

Set.mk_preimage_prod_right_eq_empty theorem

(ha : a ∉ s) : Prod.mk a ⁻¹' s ×ˢ t = ∅

Full source

@[simp]
theorem mk_preimage_prod_right_eq_empty (ha : a ∉ s) : Prod.mkProd.mk a ⁻¹' s ×ˢ t = ∅ := by
  ext b
  simp [ha]

Preimage of Cartesian Product Under Constant Function is Empty When First Component Not in Set

Informal description

For any element $a$ not in the set $s$ (i.e., $a \notin s$), the preimage of the Cartesian product $s \timesˢ t$ under the function $\lambda b \mapsto (a, b)$ is the empty set, i.e., $\{b \mid (a, b) \in s \timesˢ t\} = \emptyset$.

Set.mk_preimage_prod_left_eq_if theorem

[DecidablePred (· ∈ t)] : (fun a => (a, b)) ⁻¹' s ×ˢ t = if b ∈ t then s else ∅

Full source

theorem mk_preimage_prod_left_eq_if [DecidablePred (· ∈ t)] :
    (fun a => (a, b)) ⁻¹' s ×ˢ t = if b ∈ t then s else ∅ := by split_ifs with h <;> simp [h]

Preimage of Cartesian Product under Fixed Second Coordinate Function with Decidable Condition

Informal description

Let $s \subseteq \alpha$ and $t \subseteq \beta$ be sets, and let $b \in \beta$. The preimage of the Cartesian product $s \timesˢ t$ under the function $a \mapsto (a, b)$ is equal to $s$ if $b \in t$, and is the empty set otherwise. In other words: \[ \{a \in \alpha \mid (a, b) \in s \timesˢ t\} = \begin{cases} s & \text{if } b \in t, \\ \emptyset & \text{otherwise.} \end{cases} \]

Set.mk_preimage_prod_right_eq_if theorem

[DecidablePred (· ∈ s)] : Prod.mk a ⁻¹' s ×ˢ t = if a ∈ s then t else ∅

Full source

theorem mk_preimage_prod_right_eq_if [DecidablePred (· ∈ s)] :
    Prod.mkProd.mk a ⁻¹' s ×ˢ t = if a ∈ s then t else ∅ := by split_ifs with h <;> simp [h]

Preimage of Cartesian Product Under Right Projection with Conditional Result

Informal description

For any sets $s \subseteq \alpha$ and $t \subseteq \beta$, and any element $a \in \alpha$, the preimage of the Cartesian product $s \timesˢ t$ under the function $\lambda b \mapsto (a, b)$ is equal to $t$ if $a \in s$, and is the empty set otherwise. In other words, $\{b \in \beta \mid (a, b) \in s \timesˢ t\} = \begin{cases} t & \text{if } a \in s, \\ \emptyset & \text{otherwise.} \end{cases}$

Set.mk_preimage_prod_left_fn_eq_if theorem

[DecidablePred (· ∈ t)] (f : γ → α) : (fun a => (f a, b)) ⁻¹' s ×ˢ t = if b ∈ t then f ⁻¹' s else ∅

Full source

theorem mk_preimage_prod_left_fn_eq_if [DecidablePred (· ∈ t)] (f : γ → α) :
    (fun a => (f a, b)) ⁻¹' s ×ˢ t = if b ∈ t then f ⁻¹' s else ∅ := by
  rw [← mk_preimage_prod_left_eq_if, prod_preimage_left, preimage_preimage]

Preimage of Cartesian Product under Composed Left Projection with Conditional Result

Informal description

Let $s \subseteq \alpha$ and $t \subseteq \beta$ be sets, $f : \gamma \to \alpha$ be a function, and $b \in \beta$. The preimage of the Cartesian product $s \timesˢ t$ under the function $a \mapsto (f(a), b)$ is equal to the preimage $f^{-1}(s)$ if $b \in t$, and is the empty set otherwise. In other words: \[ \{a \in \gamma \mid (f(a), b) \in s \timesˢ t\} = \begin{cases} f^{-1}(s) & \text{if } b \in t, \\ \emptyset & \text{otherwise.} \end{cases} \]

Set.mk_preimage_prod_right_fn_eq_if theorem

[DecidablePred (· ∈ s)] (g : δ → β) : (fun b => (a, g b)) ⁻¹' s ×ˢ t = if a ∈ s then g ⁻¹' t else ∅

Full source

theorem mk_preimage_prod_right_fn_eq_if [DecidablePred (· ∈ s)] (g : δ → β) :
    (fun b => (a, g b)) ⁻¹' s ×ˢ t = if a ∈ s then g ⁻¹' t else ∅ := by
  rw [← mk_preimage_prod_right_eq_if, prod_preimage_right, preimage_preimage]

Conditional Preimage of Cartesian Product under Right Projection and Function Application

Informal description

For any sets $s \subseteq \alpha$ and $t \subseteq \beta$, any function $g : \delta \to \beta$, and any element $a \in \alpha$, the preimage of the Cartesian product $s \timesˢ t$ under the function $\lambda b \mapsto (a, g(b))$ is equal to the preimage $g^{-1}(t)$ if $a \in s$, and is the empty set otherwise. In other words: $$\{b \in \delta \mid (a, g(b)) \in s \timesˢ t\} = \begin{cases} g^{-1}(t) & \text{if } a \in s, \\ \emptyset & \text{otherwise.} \end{cases}$$

Set.preimage_swap_prod theorem

(s : Set α) (t : Set β) : Prod.swap ⁻¹' s ×ˢ t = t ×ˢ s

Full source

@[simp]
theorem preimage_swap_prod (s : Set α) (t : Set β) : Prod.swapProd.swap ⁻¹' s ×ˢ t = t ×ˢ s := by
  ext ⟨x, y⟩
  simp [and_comm]

Preimage of Cartesian Product under Swap Equals Swapped Product

Informal description

For any sets $s \subseteq \alpha$ and $t \subseteq \beta$, the preimage of the Cartesian product $s \timesˢ t$ under the swap function $\mathrm{swap} : \alpha \times \beta \to \beta \times \alpha$ equals the Cartesian product $t \timesˢ s$. In other words: $$\mathrm{swap}^{-1}(s \timesˢ t) = t \timesˢ s$$ where $\mathrm{swap}(a,b) = (b,a)$ is the function that swaps the components of a pair.

Set.image_swap_prod theorem

(s : Set α) (t : Set β) : Prod.swap '' s ×ˢ t = t ×ˢ s

Full source

@[simp]
theorem image_swap_prod (s : Set α) (t : Set β) : Prod.swapProd.swap '' s ×ˢ t = t ×ˢ s := by
  rw [image_swap_eq_preimage_swap, preimage_swap_prod]

Image of Cartesian Product under Swap Equals Swapped Product

Informal description

For any sets $s \subseteq \alpha$ and $t \subseteq \beta$, the image of the Cartesian product $s \timesˢ t$ under the swap function $\mathrm{swap} : \alpha \times \beta \to \beta \times \alpha$ equals the Cartesian product $t \timesˢ s$. In other words: $$\mathrm{swap}(s \timesˢ t) = t \timesˢ s$$ where $\mathrm{swap}(a,b) = (b,a)$ is the function that swaps the components of a pair.

Set.mapsTo_swap_prod theorem

(s : Set α) (t : Set β) : MapsTo Prod.swap (s ×ˢ t) (t ×ˢ s)

Full source

theorem mapsTo_swap_prod (s : Set α) (t : Set β) : MapsTo Prod.swap (s ×ˢ t) (t ×ˢ s) :=
  fun _ ⟨hx, hy⟩ ↦ ⟨hy, hx⟩

Swap Function Maps Cartesian Product to Its Reverse

Informal description

For any sets $s \subseteq \alpha$ and $t \subseteq \beta$, the swap function $\text{swap} : \alpha \times \beta \to \beta \times \alpha$ maps the Cartesian product $s \timesˢ t$ into $t \timesˢ s$. That is, for every $(a, b) \in s \timesˢ t$, we have $\text{swap}(a, b) = (b, a) \in t \timesˢ s$.

Set.prod_image_image_eq theorem

 {m₁ : α → γ} {m₂ : β → δ} : (m₁ '' s) ×ˢ (m₂ '' t) = (fun p : α × β => (m₁ p.1, m₂ p.2)) '' s ×ˢ t

Full source

theorem prod_image_image_eq {m₁ : α → γ} {m₂ : β → δ} :
    (m₁ '' s) ×ˢ (m₂ '' t) = (fun p : α × β => (m₁ p.1, m₂ p.2)) '' s ×ˢ t :=
  ext <| by
    simp [-exists_and_right, exists_and_right.symm, and_left_comm, and_assoc, and_comm]

Image of Cartesian Product under Component-wise Mapping

Informal description

For any functions $m_1: \alpha \to \gamma$ and $m_2: \beta \to \delta$, and sets $s \subseteq \alpha$ and $t \subseteq \beta$, the Cartesian product of the images $m_1(s) \times m_2(t)$ is equal to the image of the Cartesian product $s \times t$ under the mapping $(x,y) \mapsto (m_1(x), m_2(y))$.

Set.prod_range_range_eq theorem

{m₁ : α → γ} {m₂ : β → δ} : range m₁ ×ˢ range m₂ = range fun p : α × β => (m₁ p.1, m₂ p.2)

Full source

theorem prod_range_range_eq {m₁ : α → γ} {m₂ : β → δ} :
    range m₁ ×ˢ range m₂ = range fun p : α × β => (m₁ p.1, m₂ p.2) :=
  ext <| by simp [range]

Product of Ranges Equals Range of Product Function

Informal description

For any functions $m_1 : \alpha \to \gamma$ and $m_2 : \beta \to \delta$, the Cartesian product of their ranges equals the range of the function $(x, y) \mapsto (m_1(x), m_2(y))$. In other words, \[ \text{range}(m_1) \times \text{range}(m_2) = \text{range}\big((x, y) \mapsto (m_1(x), m_2(y))\big). \]

Set.range_prodMap theorem

{m₁ : α → γ} {m₂ : β → δ} : range (Prod.map m₁ m₂) = range m₁ ×ˢ range m₂

Full source

@[simp, mfld_simps]
theorem range_prodMap {m₁ : α → γ} {m₂ : β → δ} : range (Prod.map m₁ m₂) = range m₁ ×ˢ range m₂ :=
  prod_range_range_eq.symm

Range of Product Map Equals Product of Ranges

Informal description

For any functions $m_1 : \alpha \to \gamma$ and $m_2 : \beta \to \delta$, the range of the product map $(x, y) \mapsto (m_1(x), m_2(y))$ is equal to the Cartesian product of the ranges of $m_1$ and $m_2$. In other words, \[ \text{range}(m_1 \times m_2) = \text{range}(m_1) \times \text{range}(m_2). \]

Set.prod_range_univ_eq theorem

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

Full source

theorem prod_range_univ_eq {m₁ : α → γ} :
    range m₁ ×ˢ (univ : Set β) = range fun p : α × β => (m₁ p.1, p.2) :=
  ext <| by simp [range]

Cartesian Product of Range with Universal Set Equals Range of Paired Function

Informal description

For any function $m_1 : \alpha \to \gamma$, the Cartesian product of the range of $m_1$ with the universal set on $\beta$ is equal to the range of the function $\lambda p : \alpha \times \beta \mapsto (m_1(p.1), p.2)$. In other words: \[ \text{range}(m_1) \times \beta = \text{range}(\lambda p \mapsto (m_1(p.1), p.2)) \]

Set.prod_univ_range_eq theorem

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

Full source

theorem prod_univ_range_eq {m₂ : β → δ} :
    (univ : Set α) ×ˢ range m₂ = range fun p : α × β => (p.1, m₂ p.2) :=
  ext <| by simp [range]

Equality between Cartesian product of universal set with range and range of paired function

Informal description

For any function $m_2 : \beta \to \delta$, the Cartesian product of the universal set on $\alpha$ with the range of $m_2$ is equal to the range of the function $\lambda p : \alpha \times \beta, (p.1, m_2(p.2))$. In other words: \[ \text{univ} \timesˢ \text{range}(m_2) = \text{range}(\lambda p, (p.1, m_2(p.2))) \]

Set.range_pair_subset theorem

(f : α → β) (g : α → γ) : (range fun x => (f x, g x)) ⊆ range f ×ˢ range g

Full source

theorem range_pair_subset (f : α → β) (g : α → γ) :
    (range fun x => (f x, g x)) ⊆ range f ×ˢ range g := by
  have : (fun x => (f x, g x)) = Prod.mapProd.map f g ∘ fun x => (x, x) := funext fun x => rfl
  rw [this, ← range_prodMap]
  apply range_comp_subset_range

Range of Paired Function is Subset of Product of Ranges

Informal description

For any functions $f \colon \alpha \to \beta$ and $g \colon \alpha \to \gamma$, the range of the paired function $x \mapsto (f(x), g(x))$ is a subset of the Cartesian product of the ranges of $f$ and $g$. In other words: \[ \text{range}(\lambda x, (f(x), g(x))) \subseteq \text{range}(f) \times \text{range}(g). \]

Set.Nonempty.prod theorem

: s.Nonempty → t.Nonempty → (s ×ˢ t).Nonempty

Full source

theorem Nonempty.prod : s.Nonempty → t.Nonempty → (s ×ˢ t).Nonempty := fun ⟨x, hx⟩ ⟨y, hy⟩ =>
  ⟨(x, y), ⟨hx, hy⟩⟩

Nonempty Cartesian Product of Nonempty Sets

Informal description

For any sets $s \subseteq \alpha$ and $t \subseteq \beta$, if $s$ is nonempty and $t$ is nonempty, then their Cartesian product $s \times t$ is nonempty.

Set.Nonempty.fst theorem

: (s ×ˢ t).Nonempty → s.Nonempty

Full source

theorem Nonempty.fst : (s ×ˢ t).Nonempty → s.Nonempty := fun ⟨x, hx⟩ => ⟨x.1, hx.1⟩

Nonemptiness of First Component in Nonempty Cartesian Product

Informal description

If the Cartesian product $s \times t$ of two sets $s \subseteq \alpha$ and $t \subseteq \beta$ is nonempty, then the set $s$ is nonempty.

Set.Nonempty.snd theorem

: (s ×ˢ t).Nonempty → t.Nonempty

Full source

theorem Nonempty.snd : (s ×ˢ t).Nonempty → t.Nonempty := fun ⟨x, hx⟩ => ⟨x.2, hx.2⟩

Nonemptiness of Second Factor in Nonempty Cartesian Product

Informal description

If the Cartesian product $s \timesˢ t$ of sets $s \subseteq \alpha$ and $t \subseteq \beta$ is nonempty, then the set $t$ is nonempty.

Set.prod_nonempty_iff theorem

: (s ×ˢ t).Nonempty ↔ s.Nonempty ∧ t.Nonempty

Full source

@[simp]
theorem prod_nonempty_iff : (s ×ˢ t).Nonempty ↔ s.Nonempty ∧ t.Nonempty :=
  ⟨fun h => ⟨h.fst, h.snd⟩, fun h => h.1.prod h.2⟩

Nonemptiness Condition for Cartesian Product: $s \times t \neq \emptyset \leftrightarrow s \neq \emptyset \land t \neq \emptyset$

Informal description

The Cartesian product $s \times t$ of sets $s \subseteq \alpha$ and $t \subseteq \beta$ is nonempty if and only if both $s$ and $t$ are nonempty. In other words, $(s \times t) \neq \emptyset \leftrightarrow s \neq \emptyset \land t \neq \emptyset$.

Set.prod_eq_empty_iff theorem

: s ×ˢ t = ∅ ↔ s = ∅ ∨ t = ∅

Full source

@[simp]
theorem prod_eq_empty_iff : s ×ˢ t = ∅ ↔ s = ∅ ∨ t = ∅ := by
  simp only [not_nonempty_iff_eq_empty.symm, prod_nonempty_iff, not_and_or]

Empty Cartesian Product Condition: $s \times t = \emptyset \leftrightarrow s = \emptyset \lor t = \emptyset$

Informal description

The Cartesian product $s \times t$ of two sets $s \subseteq \alpha$ and $t \subseteq \beta$ is empty if and only if at least one of the sets $s$ or $t$ is empty. In other words, $s \times t = \emptyset \leftrightarrow s = \emptyset \lor t = \emptyset$.

Set.prod_sub_preimage_iff theorem

{W : Set γ} {f : α × β → γ} : s ×ˢ t ⊆ f ⁻¹' W ↔ ∀ a b, a ∈ s → b ∈ t → f (a, b) ∈ W

Full source

theorem prod_sub_preimage_iff {W : Set γ} {f : α × β → γ} :
    s ×ˢ t ⊆ f ⁻¹' Ws ×ˢ t ⊆ f ⁻¹' W ↔ ∀ a b, a ∈ s → b ∈ t → f (a, b) ∈ W := by simp [subset_def]

Subset Condition for Cartesian Product under Preimage

Informal description

For any sets $s \subseteq \alpha$, $t \subseteq \beta$, and $W \subseteq \gamma$, and any function $f : \alpha \times \beta \to \gamma$, the Cartesian product $s \times t$ is a subset of the preimage $f^{-1}(W)$ if and only if for all $a \in s$ and $b \in t$, the function value $f(a, b)$ belongs to $W$. In other words: $$ s \times t \subseteq f^{-1}(W) \leftrightarrow \forall a \in s, \forall b \in t, f(a, b) \in W. $$

Set.image_prodMk_subset_prod theorem

{f : α → β} {g : α → γ} {s : Set α} : (fun x => (f x, g x)) '' s ⊆ (f '' s) ×ˢ (g '' s)

Full source

theorem image_prodMk_subset_prod {f : α → β} {g : α → γ} {s : Set α} :
    (fun x => (f x, g x)) '' s(fun x => (f x, g x)) '' s ⊆ (f '' s) ×ˢ (g '' s) := by
  rintro _ ⟨x, hx, rfl⟩
  exact mk_mem_prod (mem_image_of_mem f hx) (mem_image_of_mem g hx)

Image of Product Map is Subset of Product of Images

Informal description

For any functions $f : \alpha \to \beta$ and $g : \alpha \to \gamma$, and any set $s \subseteq \alpha$, the image of $s$ under the product map $x \mapsto (f(x), g(x))$ is a subset of the Cartesian product of the images $f(s) \times g(s)$. In other words, $$\{(f(x), g(x)) \mid x \in s\} \subseteq f(s) \times g(s).$$

Set.image_prodMk_subset_prod_left theorem

(hb : b ∈ t) : (fun a => (a, b)) '' s ⊆ s ×ˢ t

Full source

theorem image_prodMk_subset_prod_left (hb : b ∈ t) : (fun a => (a, b)) '' s(fun a => (a, b)) '' s ⊆ s ×ˢ t := by
  rintro _ ⟨a, ha, rfl⟩
  exact ⟨ha, hb⟩

Image of Section Map is Subset of Cartesian Product

Informal description

For any sets $s \subseteq \alpha$ and $t \subseteq \beta$, and any element $b \in t$, the image of the function $a \mapsto (a, b)$ applied to $s$ is a subset of the Cartesian product $s \timesˢ t$.

Set.image_prodMk_subset_prod_right theorem

(ha : a ∈ s) : Prod.mk a '' t ⊆ s ×ˢ t

Full source

theorem image_prodMk_subset_prod_right (ha : a ∈ s) : Prod.mkProd.mk a '' tProd.mk a '' t ⊆ s ×ˢ t := by
  rintro _ ⟨b, hb, rfl⟩
  exact ⟨ha, hb⟩

Image of Set under Constant Pairing is Subset of Cartesian Product

Informal description

For any element $a$ in a set $s \subseteq \alpha$ and any set $t \subseteq \beta$, the image of $t$ under the function $\lambda b \mapsto (a, b)$ is a subset of the Cartesian product $s \timesˢ t$.

Set.prod_subset_preimage_fst theorem

(s : Set α) (t : Set β) : s ×ˢ t ⊆ Prod.fst ⁻¹' s

Full source

theorem prod_subset_preimage_fst (s : Set α) (t : Set β) : s ×ˢ t ⊆ Prod.fst ⁻¹' s :=
  inter_subset_left

Cartesian Product is Subset of First Projection Preimage

Informal description

For any sets $s \subseteq \alpha$ and $t \subseteq \beta$, the Cartesian product $s \times t$ is a subset of the preimage of $s$ under the first projection function $\pi_1 : \alpha \times \beta \to \alpha$.

Set.fst_image_prod_subset theorem

(s : Set α) (t : Set β) : Prod.fst '' s ×ˢ t ⊆ s

Full source

theorem fst_image_prod_subset (s : Set α) (t : Set β) : Prod.fstProd.fst '' s ×ˢ tProd.fst '' s ×ˢ t ⊆ s :=
  image_subset_iff.2 <| prod_subset_preimage_fst s t

First Projection of Cartesian Product is Subset of First Factor

Informal description

For any sets $s \subseteq \alpha$ and $t \subseteq \beta$, the image of the Cartesian product $s \times t$ under the first projection function $\pi_1 : \alpha \times \beta \to \alpha$ is a subset of $s$. In symbols: \[ \pi_1(s \times t) \subseteq s. \]

Set.fst_image_prod theorem

(s : Set β) {t : Set α} (ht : t.Nonempty) : Prod.fst '' s ×ˢ t = s

Full source

theorem fst_image_prod (s : Set β) {t : Set α} (ht : t.Nonempty) : Prod.fstProd.fst '' s ×ˢ t = s :=
  (fst_image_prod_subset _ _).antisymm fun y hy =>
    let ⟨x, hx⟩ := ht
    ⟨(y, x), ⟨hy, hx⟩, rfl⟩

First Projection of Cartesian Product Equals First Factor for Nonempty Second Factor

Informal description

For any set $s \subseteq \beta$ and nonempty set $t \subseteq \alpha$, the image of the Cartesian product $s \times t$ under the first projection function $\pi_1 : \beta \times \alpha \to \beta$ equals $s$. In symbols: \[ \pi_1(s \times t) = s. \]

Set.mapsTo_fst_prod theorem

{s : Set α} {t : Set β} : MapsTo Prod.fst (s ×ˢ t) s

Full source

lemma mapsTo_fst_prod {s : Set α} {t : Set β} : MapsTo Prod.fst (s ×ˢ t) s :=
  fun _ hx ↦ (mem_prod.1 hx).1

First Projection Maps Cartesian Product to First Factor

Informal description

For any sets $s \subseteq \alpha$ and $t \subseteq \beta$, the first projection function $\mathrm{fst} : \alpha \times \beta \to \alpha$ maps every element of the Cartesian product $s \times t$ into $s$.

Set.prod_subset_preimage_snd theorem

(s : Set α) (t : Set β) : s ×ˢ t ⊆ Prod.snd ⁻¹' t

Full source

theorem prod_subset_preimage_snd (s : Set α) (t : Set β) : s ×ˢ t ⊆ Prod.snd ⁻¹' t :=
  inter_subset_right

Cartesian Product is Subset of Second Projection Preimage

Informal description

For any sets $s \subseteq \alpha$ and $t \subseteq \beta$, the Cartesian product $s \times t$ is a subset of the preimage of $t$ under the second projection function $\mathrm{snd} : \alpha \times \beta \to \beta$. In other words, $s \times t \subseteq \mathrm{snd}^{-1}(t)$.

Set.snd_image_prod_subset theorem

(s : Set α) (t : Set β) : Prod.snd '' s ×ˢ t ⊆ t

Full source

theorem snd_image_prod_subset (s : Set α) (t : Set β) : Prod.sndProd.snd '' s ×ˢ tProd.snd '' s ×ˢ t ⊆ t :=
  image_subset_iff.2 <| prod_subset_preimage_snd s t

Image of Cartesian Product under Second Projection is Subset of Second Factor

Informal description

For any sets $s \subseteq \alpha$ and $t \subseteq \beta$, the image of the Cartesian product $s \times t$ under the second projection function $\mathrm{snd} : \alpha \times \beta \to \beta$ is a subset of $t$. In symbols: \[ \mathrm{snd}(s \times t) \subseteq t. \]

Set.snd_image_prod theorem

{s : Set α} (hs : s.Nonempty) (t : Set β) : Prod.snd '' s ×ˢ t = t

Full source

theorem snd_image_prod {s : Set α} (hs : s.Nonempty) (t : Set β) : Prod.sndProd.snd '' s ×ˢ t = t :=
  (snd_image_prod_subset _ _).antisymm fun y y_in =>
    let ⟨x, x_in⟩ := hs
    ⟨(x, y), ⟨x_in, y_in⟩, rfl⟩

Image of Cartesian Product under Second Projection Equals Second Factor for Nonempty First Factor

Informal description

For any nonempty set $s \subseteq \alpha$ and any set $t \subseteq \beta$, the image of the Cartesian product $s \times t$ under the second projection function $\mathrm{snd} : \alpha \times \beta \to \beta$ is equal to $t$. In other words: \[ \mathrm{snd}(s \times t) = t. \]

Set.mapsTo_snd_prod theorem

{s : Set α} {t : Set β} : MapsTo Prod.snd (s ×ˢ t) t

Full source

lemma mapsTo_snd_prod {s : Set α} {t : Set β} : MapsTo Prod.snd (s ×ˢ t) t :=
  fun _ hx ↦ (mem_prod.1 hx).2

Second Projection Maps Cartesian Product to Second Factor

Informal description

For any sets $s \subseteq \alpha$ and $t \subseteq \beta$, the second projection function $\mathrm{snd} : \alpha \times \beta \to \beta$ maps every element of the Cartesian product $s \times t$ into $t$.

Set.prod_diff_prod theorem

: s ×ˢ t \ s₁ ×ˢ t₁ = s ×ˢ (t \ t₁) ∪ (s \ s₁) ×ˢ t

Full source

theorem prod_diff_prod : s ×ˢ t \ s₁ ×ˢ t₁ = s ×ˢ (t \ t₁) ∪ (s \ s₁) ×ˢ t := by
  ext x
  by_cases h₁ : x.1 ∈ s₁ <;> by_cases h₂ : x.2 ∈ t₁ <;> simp [*]

Set Difference of Cartesian Products Decomposition

Informal description

For any sets $s, s_1 \subseteq \alpha$ and $t, t_1 \subseteq \beta$, the set difference of the Cartesian products $s \timesˢ t$ and $s_1 \timesˢ t_1$ is equal to the union of $s \timesˢ (t \setminus t_1)$ and $(s \setminus s_1) \timesˢ t$. In other words: $$(s \times t) \setminus (s_1 \times t_1) = (s \times (t \setminus t_1)) \cup ((s \setminus s_1) \times t)$$

Set.prod_subset_prod_iff theorem

: s ×ˢ t ⊆ s₁ ×ˢ t₁ ↔ s ⊆ s₁ ∧ t ⊆ t₁ ∨ s = ∅ ∨ t = ∅

Full source

/-- 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 prod_subset_prod_iff : s ×ˢ t ⊆ s₁ ×ˢ t₁s ×ˢ t ⊆ s₁ ×ˢ t₁ ↔ s ⊆ s₁ ∧ t ⊆ t₁ ∨ s = ∅ ∨ t = ∅ := by
  rcases (s ×ˢ t).eq_empty_or_nonempty with h | h
  · simp [h, prod_eq_empty_iff.1 h]
  have st : s.Nonempty ∧ t.Nonempty := by rwa [prod_nonempty_iff] at h
  refine ⟨fun H => Or.inl ⟨?_, ?_⟩, ?_⟩
  · have := image_subset (Prod.fst : α × β → α) H
    rwa [fst_image_prod _ st.2, fst_image_prod _ (h.mono H).snd] at this
  · have := image_subset (Prod.snd : α × β → β) H
    rwa [snd_image_prod st.1, snd_image_prod (h.mono H).fst] at this
  · intro H
    simp only [st.1.ne_empty, st.2.ne_empty, or_false] at H
    exact prod_mono H.1 H.2

Subset Condition for Cartesian Products: $s \times t \subseteq s_1 \times t_1 \leftrightarrow (s \subseteq s_1 \land t \subseteq t_1) \lor s = \emptyset \lor t = \emptyset$

Informal description

For any sets $s, s_1 \subseteq \alpha$ and $t, t_1 \subseteq \beta$, the Cartesian product $s \times t$ is a subset of $s_1 \times t_1$ if and only if either: 1. $s \subseteq s_1$ and $t \subseteq t_1$, or 2. $s$ is empty, or 3. $t$ is empty. In other words: $$ s \times t \subseteq s_1 \times t_1 \leftrightarrow (s \subseteq s_1 \land t \subseteq t_1) \lor s = \emptyset \lor t = \emptyset $$

Set.prod_eq_prod_iff_of_nonempty theorem

(h : (s ×ˢ t).Nonempty) : s ×ˢ t = s₁ ×ˢ t₁ ↔ s = s₁ ∧ t = t₁

Full source

theorem prod_eq_prod_iff_of_nonempty (h : (s ×ˢ t).Nonempty) :
    s ×ˢ t = s₁ ×ˢ t₁ ↔ s = s₁ ∧ t = t₁ := by
  constructor
  · intro heq
    have h₁ : (s₁ ×ˢ t₁ : Set _).Nonempty := by rwa [← heq]
    rw [prod_nonempty_iff] at h h₁
    rw [← fst_image_prod s h.2, ← fst_image_prod s₁ h₁.2, heq, eq_self_iff_true, true_and, ←
      snd_image_prod h.1 t, ← snd_image_prod h₁.1 t₁, heq]
  · rintro ⟨rfl, rfl⟩
    rfl

Equality of Nonempty Cartesian Products

Informal description

For nonempty sets $s \subseteq \alpha$ and $t \subseteq \beta$, the Cartesian product $s \times t$ equals another Cartesian product $s_1 \times t_1$ if and only if $s = s_1$ and $t = t_1$. In other words: $$ s \times t = s_1 \times t_1 \iff s = s_1 \land t = t_1 $$

Set.prod_eq_prod_iff theorem

: s ×ˢ t = s₁ ×ˢ t₁ ↔ s = s₁ ∧ t = t₁ ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t₁ = ∅)

Full source

theorem prod_eq_prod_iff :
    s ×ˢ t = s₁ ×ˢ t₁ ↔ s = s₁ ∧ t = t₁ ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t₁ = ∅) := by
  symm
  rcases eq_empty_or_nonempty (s ×ˢ t) with h | h
  · simp_rw [h, @eq_comm _ ∅, prod_eq_empty_iff, prod_eq_empty_iff.mp h, true_and,
      or_iff_right_iff_imp]
    rintro ⟨rfl, rfl⟩
    exact prod_eq_empty_iff.mp h
  rw [prod_eq_prod_iff_of_nonempty h]
  rw [nonempty_iff_ne_empty, Ne, prod_eq_empty_iff] at h
  simp_rw [h, false_and, or_false]

Equality Condition for Cartesian Products of Sets

Informal description

For any sets $s, s_1 \subseteq \alpha$ and $t, t_1 \subseteq \beta$, the Cartesian product $s \times t$ equals $s_1 \times t_1$ if and only if either: 1. $s = s_1$ and $t = t_1$, or 2. At least one of $s$ or $t$ is empty and at least one of $s_1$ or $t_1$ is empty. In other words: $$ s \times t = s_1 \times t_1 \iff (s = s_1 \land t = t_1) \lor (s = \emptyset \lor t = \emptyset) \land (s_1 = \emptyset \lor t_1 = \emptyset) $$

Set.prod_eq_iff_eq theorem

(ht : t.Nonempty) : s ×ˢ t = s₁ ×ˢ t ↔ s = s₁

Full source

@[simp]
theorem prod_eq_iff_eq (ht : t.Nonempty) : s ×ˢ t = s₁ ×ˢ t ↔ s = s₁ := by
  simp_rw [prod_eq_prod_iff, ht.ne_empty, and_true, or_iff_left_iff_imp, or_false]
  rintro ⟨rfl, rfl⟩
  rfl

Equality of Cartesian Products with Nonempty Second Factor

Informal description

For any nonempty set $t$ in a type $\beta$, the Cartesian product $s \times t$ is equal to $s_1 \times t$ if and only if $s = s_1$, where $s$ and $s_1$ are sets in a type $\alpha$.

Set.subset_prod theorem

{s : Set (α × β)} : s ⊆ (Prod.fst '' s) ×ˢ (Prod.snd '' s)

Full source

theorem subset_prod {s : Set (α × β)} : s ⊆ (Prod.fst '' s) ×ˢ (Prod.snd '' s) :=
  fun _ hp ↦ mem_prod.2 ⟨mem_image_of_mem _ hp, mem_image_of_mem _ hp⟩

Subset of Cartesian Product is Contained in Product of Projections

Informal description

For any subset $s$ of the Cartesian product $\alpha \times \beta$, $s$ is contained in the Cartesian product of the projections of $s$ onto $\alpha$ and $\beta$. That is, $s \subseteq (\pi_1(s)) \times (\pi_2(s))$, where $\pi_1(s) = \{a \mid \exists b, (a, b) \in s\}$ and $\pi_2(s) = \{b \mid \exists a, (a, b) \in s\}$.

Monotone.set_prod theorem

(hf : Monotone f) (hg : Monotone g) : Monotone fun x => f x ×ˢ g x

Full source

theorem _root_.Monotone.set_prod (hf : Monotone f) (hg : Monotone g) :
    Monotone fun x => f x ×ˢ g x :=
  fun _ _ h => prod_mono (hf h) (hg h)

Monotonicity of Cartesian Product of Monotone Set-Valued Functions

Informal description

Let $f$ and $g$ be monotone functions from some type to sets. Then the function $x \mapsto f(x) \times g(x)$ is also monotone, where $\times$ denotes the Cartesian product of sets.

Antitone.set_prod theorem

(hf : Antitone f) (hg : Antitone g) : Antitone fun x => f x ×ˢ g x

Full source

theorem _root_.Antitone.set_prod (hf : Antitone f) (hg : Antitone g) :
    Antitone fun x => f x ×ˢ g x :=
  fun _ _ h => prod_mono (hf h) (hg h)

Antitone Property of Cartesian Product under Antitone Functions

Informal description

If $f$ and $g$ are antitone functions (i.e., order-reversing functions), then the function $x \mapsto f(x) \times g(x)$ is also antitone, where $\times$ denotes the Cartesian product of sets.

MonotoneOn.set_prod theorem

(hf : MonotoneOn f s) (hg : MonotoneOn g s) : MonotoneOn (fun x => f x ×ˢ g x) s

Full source

theorem _root_.MonotoneOn.set_prod (hf : MonotoneOn f s) (hg : MonotoneOn g s) :
    MonotoneOn (fun x => f x ×ˢ g x) s := fun _ ha _ hb h => prod_mono (hf ha hb h) (hg ha hb h)

Monotonicity of Cartesian Product of Monotone Functions on a Set

Informal description

Let $f$ and $g$ be functions defined on a set $s$ such that $f$ is monotone on $s$ and $g$ is monotone on $s$. Then the function $x \mapsto f(x) \timesˢ g(x)$ is also monotone on $s$, where $\timesˢ$ denotes the Cartesian product of sets.

AntitoneOn.set_prod theorem

(hf : AntitoneOn f s) (hg : AntitoneOn g s) : AntitoneOn (fun x => f x ×ˢ g x) s

Full source

theorem _root_.AntitoneOn.set_prod (hf : AntitoneOn f s) (hg : AntitoneOn g s) :
    AntitoneOn (fun x => f x ×ˢ g x) s := fun _ ha _ hb h => prod_mono (hf ha hb h) (hg ha hb h)

Antitone Property Preserved Under Cartesian Product of Sets

Informal description

Let $f$ and $g$ be functions defined on a set $s$ that are antitone on $s$ (i.e., for any $x, y \in s$, if $x \leq y$ then $f(y) \subseteq f(x)$ and $g(y) \subseteq g(x)$). Then the function $x \mapsto f(x) \times g(x)$ is also antitone on $s$.

Set.diagonal_nonempty theorem

[Nonempty α] : (diagonal α).Nonempty

Full source

lemma diagonal_nonempty [Nonempty α] : (diagonal α).Nonempty :=
  Nonempty.elim ‹_› fun x => ⟨_, mem_diagonal x⟩

Nonemptiness of the Diagonal Set for Nonempty Types

Informal description

For any nonempty type $\alpha$, the diagonal set $\{(x, x) \mid x \in \alpha\}$ is nonempty.

Set.decidableMemDiagonal instance

[h : DecidableEq α] (x : α × α) : Decidable (x ∈ diagonal α)

Full source

instance decidableMemDiagonal [h : DecidableEq α] (x : α × α) : Decidable (x ∈ diagonal α) :=
  h x.1 x.2

Decidability of Diagonal Membership

Informal description

For any type $\alpha$ with decidable equality, given a pair $x \in \alpha \times \alpha$, it is decidable whether $x$ belongs to the diagonal of $\alpha$.

Set.preimage_coe_coe_diagonal theorem

(s : Set α) : Prod.map (fun x : s => (x : α)) (fun x : s => (x : α)) ⁻¹' diagonal α = diagonal s

Full source

theorem preimage_coe_coe_diagonal (s : Set α) :
    Prod.mapProd.map (fun x : s => (x : α)) (fun x : s => (x : α)) ⁻¹' diagonal α = diagonal s := by
  ext ⟨⟨x, hx⟩, ⟨y, hy⟩⟩
  simp [Set.diagonal]

Preimage of Diagonal under Inclusion Map Equals Diagonal of Subset

Informal description

For any subset $s$ of a type $\alpha$, the preimage of the diagonal $\{(x, x) \mid x \in \alpha\}$ under the product map $(x, x) \mapsto (x, x)$ (where $x$ is considered as an element of $s$) is equal to the diagonal $\{(x, x) \mid x \in s\}$ of $s$.

Set.range_diag theorem

: (range fun x => (x, x)) = diagonal α

Full source

@[simp]
theorem range_diag : (range fun x => (x, x)) = diagonal α := by
  ext ⟨x, y⟩
  simp [diagonal, eq_comm]

Range of Diagonal Map Equals Diagonal Set

Informal description

The range of the diagonal map $x \mapsto (x, x)$ is equal to the diagonal set $\{(x, x) \mid x \in \alpha\}$ of the type $\alpha$.

Set.diagonal_subset_iff theorem

{s} : diagonal α ⊆ s ↔ ∀ x, (x, x) ∈ s

Full source

theorem diagonal_subset_iff {s} : diagonaldiagonal α ⊆ sdiagonal α ⊆ s ↔ ∀ x, (x, x) ∈ s := by
  rw [← range_diag, range_subset_iff]

Diagonal Subset Criterion: $\mathrm{diagonal}(\alpha) \subseteq s \leftrightarrow \forall x, (x, x) \in s$

Informal description

For any subset $s$ of $\alpha \times \alpha$, the diagonal $\{(x, x) \mid x \in \alpha\}$ is contained in $s$ if and only if for every $x \in \alpha$, the pair $(x, x)$ belongs to $s$.

Set.prod_subset_compl_diagonal_iff_disjoint theorem

: s ×ˢ t ⊆ (diagonal α)ᶜ ↔ Disjoint s t

Full source

@[simp]
theorem prod_subset_compl_diagonal_iff_disjoint : s ×ˢ t ⊆ (diagonal α)ᶜs ×ˢ t ⊆ (diagonal α)ᶜ ↔ Disjoint s t :=
  prod_subset_iff.trans disjoint_iff_forall_ne.symm

Cartesian Product Disjointness Criterion: $s \times t \subseteq \Delta^c \leftrightarrow s \cap t = \emptyset$

Informal description

For any two sets $s$ and $t$ in a type $\alpha$, the Cartesian product $s \times t$ is contained in the complement of the diagonal $\{(x,x) \mid x \in \alpha\}$ if and only if $s$ and $t$ are disjoint (i.e., $s \cap t = \emptyset$).

Set.diag_preimage_prod theorem

(s t : Set α) : (fun x => (x, x)) ⁻¹' s ×ˢ t = s ∩ t

Full source

@[simp]
theorem diag_preimage_prod (s t : Set α) : (fun x => (x, x)) ⁻¹' s ×ˢ t = s ∩ t :=
  rfl

Preimage of Cartesian Product under Diagonal Map Equals Intersection

Informal description

For any sets $s$ and $t$ in a type $\alpha$, the preimage of the Cartesian product $s \timesˢ t$ under the diagonal map $x \mapsto (x, x)$ is equal to the intersection $s \cap t$.

Set.diag_preimage_prod_self theorem

(s : Set α) : (fun x => (x, x)) ⁻¹' s ×ˢ s = s

Full source

theorem diag_preimage_prod_self (s : Set α) : (fun x => (x, x)) ⁻¹' s ×ˢ s = s :=
  inter_self s

Preimage of $s \timesˢ s$ under Diagonal Map Equals $s$

Informal description

For any set $s$ in a type $\alpha$, the preimage of the Cartesian product $s \timesˢ s$ under the diagonal map $x \mapsto (x, x)$ is equal to $s$ itself, i.e., $\{x \in \alpha \mid (x, x) \in s \timesˢ s\} = s$.

Set.diag_image theorem

(s : Set α) : (fun x => (x, x)) '' s = diagonal α ∩ s ×ˢ s

Full source

theorem diag_image (s : Set α) : (fun x => (x, x)) '' s = diagonaldiagonal α ∩ s ×ˢ s := by
  rw [← range_diag, ← image_preimage_eq_range_inter, diag_preimage_prod_self]

Image of Set under Diagonal Map Equals Diagonal Intersection with Cartesian Square

Informal description

For any set $s$ in a type $\alpha$, the image of $s$ under the diagonal map $x \mapsto (x, x)$ is equal to the intersection of the diagonal set $\{(x, x) \mid x \in \alpha\}$ with the Cartesian product $s \timesˢ s$.

Set.diagonal_eq_univ_iff theorem

: diagonal α = univ ↔ Subsingleton α

Full source

theorem diagonal_eq_univ_iff : diagonaldiagonal α = univ ↔ Subsingleton α := by
  simp only [subsingleton_iff, eq_univ_iff_forall, Prod.forall, mem_diagonal_iff]

Diagonal Equals Universal Set iff Type is Subsingleton

Informal description

The diagonal of a type $\alpha$ equals the universal set if and only if $\alpha$ is a subsingleton (i.e., all elements of $\alpha$ are equal).

Set.diagonal_eq_univ theorem

[Subsingleton α] : diagonal α = univ

Full source

theorem diagonal_eq_univ [Subsingleton α] : diagonal α = univ := diagonal_eq_univ_iff.2 ‹_›

Diagonal Equals Universal Set for Subsingleton Types

Informal description

If $\alpha$ is a subsingleton type (i.e., all elements of $\alpha$ are equal), then the diagonal set $\{(x, x) \mid x \in \alpha\}$ is equal to the universal set $\alpha \times \alpha$.

Set.range_const_eq_diagonal theorem

{α β : Type*} [hβ : Nonempty β] : range (const α) = {f : α → β | ∀ x y, f x = f y}

Full source

/-- A function is `Function.const α a` for some `a` if and only if `∀ x y, f x = f y`. -/
theorem range_const_eq_diagonal {α β : Type*} [hβ : Nonempty β] :
    range (const α) = {f : α → β | ∀ x y, f x = f y} := by
  refine (range_eq_iff _ _).mpr ⟨fun _ _ _ ↦ rfl, fun f hf ↦ ?_⟩
  rcases isEmpty_or_nonempty α with h|⟨⟨a⟩⟩
  · exact hβ.elim fun b ↦ ⟨b, Subsingleton.elim _ _⟩
  · exact ⟨f a, funext fun x ↦ hf _ _⟩

Range of Constant Function Equals Set of Constant-Valued Functions

Informal description

For nonempty types $\alpha$ and $\beta$, the range of the constant function $\mathrm{const}_\alpha : \beta \to (\alpha \to \beta)$ is equal to the set of all functions $f : \alpha \to \beta$ that satisfy $\forall x y, f(x) = f(y)$.

Function.Pullback abbrev

(f : X → Y) (g : Z → Y)

Full source

/-- The fiber product $X \times_Y Z$. -/
abbrev Function.Pullback (f : X → Y) (g : Z → Y) := {p : X × Z // f p.1 = g p.2}

Fiber Product of Functions: $X \times_Y Z$

Informal description

Given two functions $f \colon X \to Y$ and $g \colon Z \to Y$ with the same codomain, the pullback (or fiber product) $X \times_Y Z$ is the set of pairs $(x, z) \in X \times Z$ such that $f(x) = g(z)$.

Function.PullbackSelf abbrev

(f : X → Y)

Full source

/-- The fiber product $X \times_Y X$. -/
abbrev Function.PullbackSelf (f : X → Y) := f.Pullback f

Fiber Product of a Function with Itself: $X \times_Y X$

Informal description

Given a function $f \colon X \to Y$, the fiber product $X \times_Y X$ is the set of pairs $(x, x') \in X \times X$ such that $f(x) = f(x')$.

Function.Pullback.fst definition

{f : X → Y} {g : Z → Y} (p : f.Pullback g) : X

Full source

/-- The projection from the fiber product to the first factor. -/
def Function.Pullback.fst {f : X → Y} {g : Z → Y} (p : f.Pullback g) : X := p.val.1

First projection from fiber product

Informal description

The projection map from the fiber product $X \times_Y Z$ to the first factor $X$, sending a pair $(x, z)$ to $x$.

Function.Pullback.snd definition

{f : X → Y} {g : Z → Y} (p : f.Pullback g) : Z

Full source

/-- The projection from the fiber product to the second factor. -/
def Function.Pullback.snd {f : X → Y} {g : Z → Y} (p : f.Pullback g) : Z := p.val.2

Second projection from fiber product

Informal description

Given two functions $f \colon X \to Y$ and $g \colon Z \to Y$, and an element $p$ of their fiber product (i.e., a pair $(x,z)$ such that $f(x) = g(z)$), this function returns the second component $z \in Z$ of the pair.

Function.pullback_comm_sq theorem

(f : X → Y) (g : Z → Y) : f ∘ @fst X Y Z f g = g ∘ @snd X Y Z f g

Full source

lemma Function.pullback_comm_sq (f : X → Y) (g : Z → Y) :
    f ∘ @fst X Y Z f g = g ∘ @snd X Y Z f g := funext fun p ↦ p.2

Commutativity of Fiber Product Diagram

Informal description

For any two functions $f \colon X \to Y$ and $g \colon Z \to Y$, the composition of $f$ with the first projection from the fiber product $X \times_Y Z$ equals the composition of $g$ with the second projection from the same fiber product. In other words, the following diagram commutes: \[ \begin{CD} X \times_Y Z @>{\text{fst}}>> X \\ @V{\text{snd}}VV @VV{f}V \\ Z @>>{g}> Y \end{CD} \]

toPullbackDiag definition

(f : X → Y) (x : X) : f.Pullback f

Full source

/-- The diagonal map $\Delta: X \to X \times_Y X$. -/
@[simps]
def toPullbackDiag (f : X → Y) (x : X) : f.Pullback f := ⟨(x, x), rfl⟩

Diagonal map into fiber product

Informal description

For a function $f \colon X \to Y$ and an element $x \in X$, the map $\text{toPullbackDiag}$ sends $x$ to the pair $(x, x)$ in the fiber product $X \times_Y X$, where the equality $f(x) = f(x)$ holds trivially.

Function.pullbackDiagonal definition

(f : X → Y) : Set (f.Pullback f)

Full source

/-- The diagonal $\Delta(X) \subseteq X \times_Y X$. -/
def Function.pullbackDiagonal (f : X → Y) : Set (f.Pullback f) := {p | p.fst = p.snd}

Diagonal of a function's fiber product

Informal description

For a function $f \colon X \to Y$, the set $\Delta_f \subseteq X \times_Y X$ consists of all pairs $(x_1, x_2)$ such that $f(x_1) = f(x_2)$ and $x_1 = x_2$. In other words, it is the diagonal subset of the fiber product $X \times_Y X$, where both components of the pair are equal.

Function.mapPullback definition

 {X₁ X₂ Y₁ Y₂ Z₁ Z₂} {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 : f₁.Pullback g₁) : f₂.Pullback g₂

Full source

/-- 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$. -/
def Function.mapPullback {X₁ X₂ Y₁ Y₂ Z₁ Z₂}
    {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 : f₁.Pullback g₁) : f₂.Pullback g₂ :=
  ⟨(mapX p.fst, mapZ p.snd),
    (congr_fun commX _).trans <| (congr_arg mapY p.2).trans <| congr_fun commZ.symm _⟩

Induced map between fiber products via commuting squares

Informal description

Given three pairs of functions $(f_1 \colon X_1 \to Y_1, g_1 \colon Z_1 \to Y_1)$ and $(f_2 \colon X_2 \to Y_2, g_2 \colon Z_2 \to Y_2)$, and three maps $\text{mapX} \colon X_1 \to X_2$, $\text{mapY} \colon Y_1 \to Y_2$, $\text{mapZ} \colon Z_1 \to Z_2$ that commute with $f_1, f_2$ and $g_1, g_2$ respectively, there is an induced map from the fiber product $X_1 \times_{Y_1} Z_1$ to $X_2 \times_{Y_2} Z_2$. Specifically, for any element $(x, z) \in X_1 \times_{Y_1} Z_1$ (satisfying $f_1(x) = g_1(z)$), the map sends $(x, z)$ to $(\text{mapX}(x), \text{mapZ}(z)) \in X_2 \times_{Y_2} Z_2$, which satisfies $f_2(\text{mapX}(x)) = g_2(\text{mapZ}(z))$ due to the commutativity conditions.

Function.PullbackSelf.map_fst definition

{f : X → Y} {g : Z → Y} : (@snd X Y Z f g).PullbackSelf → f.PullbackSelf

Full source

/-- The projection $(X \times_Y Z) \times_Z (X \times_Y Z) \to X \times_Y X$. -/
def Function.PullbackSelf.map_fst {f : X → Y} {g : Z → Y} :
    (@snd X Y Z f g).PullbackSelf → f.PullbackSelf :=
  mapPullback fst g fst (pullback_comm_sq f g) (pullback_comm_sq f g)

First projection map between fiber products

Informal description

Given functions $f \colon X \to Y$ and $g \colon Z \to Y$, the map sends a pair $(p_1, p_2)$ in the fiber product $(X \times_Y Z) \times_X (X \times_Y Z)$ (where $p_1$ and $p_2$ are pairs in $X \times_Y Z$ with equal second components) to the pair $(x_1, x_2)$ in $X \times_Y X$, where $x_1$ and $x_2$ are the first components of $p_1$ and $p_2$ respectively. This map is constructed using the first projection from the fiber product.

Function.PullbackSelf.map_snd definition

{f : X → Y} {g : Z → Y} : (@fst X Y Z f g).PullbackSelf → g.PullbackSelf

Full source

/-- The projection $(X \times_Y Z) \times_X (X \times_Y Z) \to Z \times_Y Z$. -/
def Function.PullbackSelf.map_snd {f : X → Y} {g : Z → Y} :
    (@fst X Y Z f g).PullbackSelf → g.PullbackSelf :=
  mapPullback snd f snd (pullback_comm_sq f g).symm (pullback_comm_sq f g).symm

Second projection map between fiber products

Informal description

Given functions $f \colon X \to Y$ and $g \colon Z \to Y$, the map sends a pair $(p_1, p_2)$ in the fiber product $(X \times_Y Z) \times_X (X \times_Y Z)$ (where $p_1$ and $p_2$ are pairs in $X \times_Y Z$ with equal first components) to the pair $(z_1, z_2)$ in $Z \times_Y Z$, where $z_1$ and $z_2$ are the second components of $p_1$ and $p_2$ respectively. This map is constructed using the second projection from the fiber product.

preimage_map_fst_pullbackDiagonal theorem

{f : X → Y} {g : Z → Y} : @map_fst X Y Z f g ⁻¹' pullbackDiagonal f = pullbackDiagonal (@snd X Y Z f g)

Full source

theorem preimage_map_fst_pullbackDiagonal {f : X → Y} {g : Z → Y} :
    @map_fst X Y Z f g ⁻¹' pullbackDiagonal f = pullbackDiagonal (@snd X Y Z f g) := by
  ext ⟨⟨p₁, p₂⟩, he⟩
  simp_rw [pullbackDiagonal, mem_setOf, Subtype.ext_iff, Prod.ext_iff]
  exact (and_iff_left he).symm

Preimage of Diagonal under First Projection in Fiber Product

Informal description

For any functions $f \colon X \to Y$ and $g \colon Z \to Y$, the preimage of the diagonal set $\Delta_f \subseteq X \times_Y X$ under the first projection map $\mathrm{map\_fst} \colon (X \times_Y Z) \times_X (X \times_Y Z) \to X \times_Y X$ is equal to the diagonal set $\Delta_{\mathrm{snd}} \subseteq (X \times_Y Z) \times_X (X \times_Y Z)$, where $\mathrm{snd}$ denotes the second projection from the fiber product $X \times_Y Z$.

Function.Injective.preimage_pullbackDiagonal theorem

 {f : X → Y} {g : Z → X} (inj : g.Injective) :
  mapPullback g id g (by rfl) (by rfl) ⁻¹' pullbackDiagonal f = pullbackDiagonal (f ∘ g)

Full source

theorem Function.Injective.preimage_pullbackDiagonal {f : X → Y} {g : Z → X} (inj : g.Injective) :
    mapPullbackmapPullback g id g (by rfl) (by rfl) ⁻¹' pullbackDiagonal f = pullbackDiagonal (f ∘ g) :=
  ext fun _ ↦ inj.eq_iff

Preimage of Diagonal under Induced Map Equals Diagonal for Composition

Informal description

Let $f \colon X \to Y$ and $g \colon Z \to X$ be functions, with $g$ injective. Then the preimage of the diagonal set $\Delta_f \subseteq X \times_Y X$ under the induced map $g \times_Y g \colon Z \times_Y Z \to X \times_Y X$ is equal to the diagonal set $\Delta_{f \circ g} \subseteq Z \times_Y Z$. Here: - $\Delta_f = \{(x_1, x_2) \in X \times_Y X \mid x_1 = x_2\}$ is the diagonal in the fiber product $X \times_Y X$ - $\Delta_{f \circ g} = \{(z_1, z_2) \in Z \times_Y Z \mid z_1 = z_2\}$ is the diagonal in the fiber product $Z \times_Y Z$ - The map $g \times_Y g$ sends $(z_1, z_2) \in Z \times_Y Z$ to $(g(z_1), g(z_2)) \in X \times_Y X$

image_toPullbackDiag theorem

(f : X → Y) (s : Set X) : toPullbackDiag f '' s = pullbackDiagonal f ∩ Subtype.val ⁻¹' s ×ˢ s

Full source

theorem image_toPullbackDiag (f : X → Y) (s : Set X) :
    toPullbackDiagtoPullbackDiag f '' s = pullbackDiagonalpullbackDiagonal f ∩ Subtype.val ⁻¹' s ×ˢ s := by
  ext x
  constructor
  · rintro ⟨x, hx, rfl⟩
    exact ⟨rfl, hx, hx⟩
  · obtain ⟨⟨x, y⟩, h⟩ := x
    rintro ⟨rfl : x = y, h2x⟩
    exact mem_image_of_mem _ h2x.1

Image of Diagonal Map in Fiber Product Equals Diagonal Intersection with Preimage of Cartesian Square

Informal description

For any function $f \colon X \to Y$ and any subset $s \subseteq X$, the image of $s$ under the diagonal map $\text{toPullbackDiag}_f \colon X \to X \times_Y X$ (defined by $x \mapsto (x, x)$) is equal to the intersection of the diagonal set $\Delta_f = \{(x_1, x_2) \in X \times_Y X \mid x_1 = x_2\}$ with the preimage of the Cartesian product $s \times s$ under the projection map $\text{Subtype.val} \colon X \times_Y X \to X \times X$.

range_toPullbackDiag theorem

(f : X → Y) : range (toPullbackDiag f) = pullbackDiagonal f

Full source

theorem range_toPullbackDiag (f : X → Y) : range (toPullbackDiag f) = pullbackDiagonal f := by
  rw [← image_univ, image_toPullbackDiag, univ_prod_univ, preimage_univ, inter_univ]

Range of Diagonal Map Equals Diagonal in Fiber Product

Informal description

For any function $f \colon X \to Y$, the range of the diagonal map $\text{toPullbackDiag}_f \colon X \to X \times_Y X$ (defined by $x \mapsto (x, x)$) is equal to the diagonal set $\Delta_f = \{(x_1, x_2) \in X \times_Y X \mid x_1 = x_2\}$ of the fiber product $X \times_Y X$.

injective_toPullbackDiag theorem

(f : X → Y) : (toPullbackDiag f).Injective

Full source

theorem injective_toPullbackDiag (f : X → Y) : (toPullbackDiag f).Injective :=
  fun _ _ h ↦ congr_arg Prod.fst (congr_arg Subtype.val h)

Injectivity of the Diagonal Map into Fiber Product

Informal description

For any function $f \colon X \to Y$, the diagonal map $\text{toPullbackDiag}_f \colon X \to X \times_Y X$ defined by $x \mapsto (x, x)$ is injective.

Set.offDiag_mono theorem

: Monotone (offDiag : Set α → Set (α × α))

Full source

theorem offDiag_mono : Monotone (offDiag : Set α → Set (α × α)) := fun _ _ h _ =>
  And.imp (@h _) <| And.imp_left <| @h _

Monotonicity of the Off-Diagonal Set Construction

Informal description

The function that maps a set $s$ to its off-diagonal $\{(a, b) \in s \times s \mid a \neq b\}$ is monotone. That is, for any sets $s$ and $t$ in $\alpha$, if $s \subseteq t$, then the off-diagonal of $s$ is a subset of the off-diagonal of $t$.

Set.offDiag_nonempty theorem

: s.offDiag.Nonempty ↔ s.Nontrivial

Full source

@[simp]
theorem offDiag_nonempty : s.offDiag.Nonempty ↔ s.Nontrivial := by
  simp [offDiag, Set.Nonempty, Set.Nontrivial]

Nonempty Off-Diagonal Characterizes Nontrivial Sets

Informal description

For any set $s$, the off-diagonal of $s$ is nonempty if and only if $s$ is nontrivial (i.e., contains at least two distinct elements).

Set.offDiag_eq_empty theorem

: s.offDiag = ∅ ↔ s.Subsingleton

Full source

@[simp]
theorem offDiag_eq_empty : s.offDiag = ∅ ↔ s.Subsingleton := by
  rw [← not_nonempty_iff_eq_empty, ← not_nontrivial_iff, offDiag_nonempty.not]

Empty Off-Diagonal Characterizes Subsingleton Sets

Informal description

For any set $s$, the off-diagonal of $s$ is empty if and only if $s$ is a subsingleton (i.e., contains at most one element).

Set.offDiag_subset_prod theorem

: s.offDiag ⊆ s ×ˢ s

Full source

theorem offDiag_subset_prod : s.offDiag ⊆ s ×ˢ s := fun _ hx => ⟨hx.1, hx.2.1⟩

Off-diagonal is Subset of Cartesian Square

Informal description

For any set $s$ over a type $\alpha$, the off-diagonal of $s$ is a subset of the Cartesian product $s \times s$.

Set.offDiag_eq_sep_prod theorem

: s.offDiag = {x ∈ s ×ˢ s | x.1 ≠ x.2}

Full source

theorem offDiag_eq_sep_prod : s.offDiag = { x ∈ s ×ˢ s | x.1 ≠ x.2 } :=
  ext fun _ => and_assoc.symm

Off-diagonal as Filtered Cartesian Product: $s.\text{offDiag} = \{(x,y) \in s \times s \mid x \neq y\}$

Informal description

For any set $s$ over a type $\alpha$, the off-diagonal of $s$ is equal to the set of all pairs $(x_1, x_2)$ in the Cartesian product $s \times s$ such that $x_1 \neq x_2$. In other words, $s.\text{offDiag} = \{(x_1, x_2) \in s \times s \mid x_1 \neq x_2\}$.

Set.offDiag_empty theorem

: (∅ : Set α).offDiag = ∅

Full source

@[simp]
theorem offDiag_empty : (∅ : Set α).offDiag = ∅ := by simp

Empty Set's Off-Diagonal is Empty

Informal description

For any type $\alpha$, the off-diagonal of the empty set is the empty set, i.e., $\mathrm{offDiag}(\emptyset) = \emptyset$.

Set.offDiag_singleton theorem

(a : α) : ({ a } : Set α).offDiag = ∅

Full source

@[simp]
theorem offDiag_singleton (a : α) : ({a} : Set α).offDiag = ∅ := by simp

Off-diagonal of a Singleton Set is Empty

Informal description

For any element $a$ of a type $\alpha$, the off-diagonal of the singleton set $\{a\}$ is the empty set, i.e., $\{a\}.offDiag = \emptyset$.

Set.offDiag_univ theorem

: (univ : Set α).offDiag = (diagonal α)ᶜ

Full source

@[simp]
theorem offDiag_univ : (univ : Set α).offDiag = (diagonal α)ᶜ :=
  ext <| by simp

Off-diagonal of Universal Set Equals Complement of Diagonal

Informal description

The off-diagonal of the universal set on a type $\alpha$ is equal to the complement of the diagonal of $\alpha$, i.e., $\mathrm{offDiag}(\mathrm{univ}) = (\mathrm{diagonal}(\alpha))^c$.

Set.prod_sdiff_diagonal theorem

: s ×ˢ s \ diagonal α = s.offDiag

Full source

@[simp]
theorem prod_sdiff_diagonal : s ×ˢ s \ diagonal α = s.offDiag :=
  ext fun _ => and_assoc

Cartesian Product Minus Diagonal Equals Off-Diagonal

Informal description

For any set $s$ in a type $\alpha$, the set difference between the Cartesian product $s \times s$ and the diagonal of $\alpha$ is equal to the off-diagonal of $s$, i.e., $(s \times s) \setminus \mathrm{diagonal}(\alpha) = \mathrm{offDiag}(s)$.

Set.disjoint_diagonal_offDiag theorem

: Disjoint (diagonal α) s.offDiag

Full source

@[simp]
theorem disjoint_diagonal_offDiag : Disjoint (diagonal α) s.offDiag :=
  disjoint_left.mpr fun _ hd ho => ho.2.2 hd

Diagonal and Off-Diagonal are Disjoint

Informal description

For any set $s$ in a type $\alpha$, the diagonal of $\alpha$ and the off-diagonal of $s$ are disjoint, i.e., $\mathrm{diagonal}(\alpha) \cap \mathrm{offDiag}(s) = \emptyset$.

Set.offDiag_inter theorem

: (s ∩ t).offDiag = s.offDiag ∩ t.offDiag

Full source

theorem offDiag_inter : (s ∩ t).offDiag = s.offDiag ∩ t.offDiag :=
  ext fun x => by
    simp only [mem_offDiag, mem_inter_iff]
    tauto

Intersection of Off-Diagonals Equals Off-Diagonal of Intersection

Informal description

For any sets $s$ and $t$ over a type $\alpha$, the off-diagonal of their intersection equals the intersection of their off-diagonals, i.e., $$(s \cap t).\text{offDiag} = s.\text{offDiag} \cap t.\text{offDiag}.$$

Set.offDiag_union theorem

(h : Disjoint s t) : (s ∪ t).offDiag = s.offDiag ∪ t.offDiag ∪ s ×ˢ t ∪ t ×ˢ s

Full source

theorem offDiag_union (h : Disjoint s t) :
    (s ∪ t).offDiag = s.offDiag ∪ t.offDiags.offDiag ∪ t.offDiag ∪ s ×ˢ ts.offDiag ∪ t.offDiag ∪ s ×ˢ t ∪ t ×ˢ s := by
  ext x
  simp only [mem_offDiag, mem_union, ne_eq, mem_prod]
  constructor
  · rintro ⟨h0|h0, h1|h1, h2⟩ <;> simp [h0, h1, h2]
  · rintro (((⟨h0, h1, h2⟩|⟨h0, h1, h2⟩)|⟨h0, h1⟩)|⟨h0, h1⟩) <;> simp [*]
    · rintro h3
      rw [h3] at h0
      exact Set.disjoint_left.mp h h0 h1
    · rintro h3
      rw [h3] at h0
      exact (Set.disjoint_right.mp h h0 h1).elim

Off-diagonal of Union of Disjoint Sets

Informal description

For any two disjoint sets $s$ and $t$ over a type $\alpha$, the off-diagonal of their union is equal to the union of their off-diagonals and their Cartesian products in both orders, i.e., $$(s \cup t).\text{offDiag} = s.\text{offDiag} \cup t.\text{offDiag} \cup (s \times t) \cup (t \times s).$$

Set.offDiag_insert theorem

(ha : a ∉ s) : (insert a s).offDiag = s.offDiag ∪ { a } ×ˢ s ∪ s ×ˢ { a }

Full source

theorem offDiag_insert (ha : a ∉ s) : (insert a s).offDiag = s.offDiag ∪ {a} ×ˢ ss.offDiag ∪ {a} ×ˢ s ∪ s ×ˢ {a} := by
  rw [insert_eq, union_comm, offDiag_union, offDiag_singleton, union_empty, union_right_comm]
  rw [disjoint_left]
  rintro b hb (rfl : b = a)
  exact ha hb

Off-diagonal of Inserted Set Equals Union of Off-diagonal and Cartesian Products

Informal description

For any element $a$ not in a set $s$ over a type $\alpha$, the off-diagonal of the set obtained by inserting $a$ into $s$ is equal to the union of the off-diagonal of $s$ and the Cartesian products $\{a\} \times s$ and $s \times \{a\}$. That is, $$(\{a\} \cup s).\text{offDiag} = s.\text{offDiag} \cup (\{a\} \times s) \cup (s \times \{a\}).$$

Set.empty_pi theorem

(s : ∀ i, Set (α i)) : pi ∅ s = univ

Full source

@[simp]
theorem empty_pi (s : ∀ i, Set (α i)) : pi ∅ s = univ := by
  ext
  simp [pi]

Empty Product of Sets Equals Universal Set

Informal description

For any family of sets $(t_i)_{i \in \iota}$ where each $t_i$ is a subset of $\alpha_i$, the product of the empty index set is equal to the universal set in the dependent function space $\prod_{i \in \iota} \alpha_i$. That is, \[ \prod_{i \in \emptyset} t_i = \prod_{i \in \iota} \alpha_i. \]

Set.subsingleton_univ_pi theorem

(ht : ∀ i, (t i).Subsingleton) : (univ.pi t).Subsingleton

Full source

theorem subsingleton_univ_pi (ht : ∀ i, (t i).Subsingleton) :
    (univ.pi t).Subsingleton := fun _f hf _g hg ↦ funext fun i ↦
  (ht i) (hf _ <| mem_univ _) (hg _ <| mem_univ _)

Product of Subsingletons is Subsingleton

Informal description

For any family of sets $(t_i)_{i \in \iota}$ where each $t_i$ is a subsingleton (i.e., contains at most one element), the product set $\prod_{i \in \iota} t_i$ is also a subsingleton.

Set.pi_univ theorem

(s : Set ι) : (pi s fun i => (univ : Set (α i))) = univ

Full source

@[simp]
theorem pi_univ (s : Set ι) : (pi s fun i => (univ : Set (α i))) = univ :=
  eq_univ_of_forall fun _ _ _ => mem_univ _

Universal Product of Universal Sets

Informal description

For any set $s \subseteq \iota$, the product of the universal sets over $s$ equals the universal set in the dependent function space $\prod_{i \in \iota} \alpha_i$. That is, \[ \prod_{i \in s} \alpha_i = \prod_{i \in \iota} \alpha_i. \]

Set.pi_univ_ite theorem

 (s : Set ι) [DecidablePred (· ∈ s)] (t : ∀ i, Set (α i)) : (pi univ fun i => if i ∈ s then t i else univ) = s.pi t

Full source

@[simp]
theorem pi_univ_ite (s : Set ι) [DecidablePred (· ∈ s)] (t : ∀ i, Set (α i)) :
    (pi univ fun i => if i ∈ s then t i else univ) = s.pi t := by
  ext; simp_rw [Set.mem_pi]; apply forall_congr'; intro i; split_ifs with h <;> simp [h]

Product of Sets with Conditional Universes Equals Restricted Product

Informal description

For any set $s \subseteq \iota$ with a decidable membership predicate, and any family of sets $t_i \subseteq \alpha_i$ indexed by $i \in \iota$, the product of sets over the universal set $\iota$ defined by: \[ \prod_{i \in \iota} \begin{cases} t_i & \text{if } i \in s \\ \alpha_i & \text{otherwise} \end{cases} \] is equal to the product of sets $\prod_{i \in s} t_i$.

Set.pi_mono theorem

(h : ∀ i ∈ s, t₁ i ⊆ t₂ i) : pi s t₁ ⊆ pi s t₂

Full source

theorem pi_mono (h : ∀ i ∈ s, t₁ i ⊆ t₂ i) : pipi s t₁ ⊆ pi s t₂ := fun _ hx i hi => h i hi <| hx i hi

Monotonicity of Product Sets: $\prod_{i \in s} t_1(i) \subseteq \prod_{i \in s} t_2(i)$ when $t_1(i) \subseteq t_2(i)$ for all $i \in s$

Informal description

For any index set $s$ and any two families of sets $t_1(i)$ and $t_2(i)$ indexed by $i \in s$, if $t_1(i) \subseteq t_2(i)$ for all $i \in s$, then the product set $\prod_{i \in s} t_1(i)$ is a subset of $\prod_{i \in s} t_2(i)$.

Set.pi_inter_distrib theorem

: (s.pi fun i => t i ∩ t₁ i) = s.pi t ∩ s.pi t₁

Full source

theorem pi_inter_distrib : (s.pi fun i => t i ∩ t₁ i) = s.pi t ∩ s.pi t₁ :=
  ext fun x => by simp only [forall_and, mem_pi, mem_inter_iff]

Distributivity of Product over Intersection: $\prod_{i \in s} (t_i \cap t'_i) = (\prod_{i \in s} t_i) \cap (\prod_{i \in s} t'_i)$

Informal description

For any index set $s$ and any two families of sets $t_i$ and $t'_i$ indexed by $i \in s$, the product of the intersections equals the intersection of the products: \[ \prod_{i \in s} (t_i \cap t'_i) = \left(\prod_{i \in s} t_i\right) \cap \left(\prod_{i \in s} t'_i\right). \]

Set.pi_congr theorem

(h : s₁ = s₂) (h' : ∀ i ∈ s₁, t₁ i = t₂ i) : s₁.pi t₁ = s₂.pi t₂

Full source

theorem pi_congr (h : s₁ = s₂) (h' : ∀ i ∈ s₁, t₁ i = t₂ i) : s₁.pi t₁ = s₂.pi t₂ :=
  h ▸ ext fun _ => forall₂_congr fun i hi => h' i hi ▸ Iff.rfl

Equality of Product Sets under Index and Component Equality

Informal description

Let $s_1$ and $s_2$ be index sets, and for each $i \in s_1$, let $t_1(i)$ and $t_2(i)$ be subsets of $\alpha_i$. If $s_1 = s_2$ and for every $i \in s_1$ we have $t_1(i) = t_2(i)$, then the product sets $\prod_{i \in s_1} t_1(i)$ and $\prod_{i \in s_2} t_2(i)$ are equal.

Set.pi_eq_empty theorem

(hs : i ∈ s) (ht : t i = ∅) : s.pi t = ∅

Full source

theorem pi_eq_empty (hs : i ∈ s) (ht : t i = ∅) : s.pi t = ∅ := by
  ext f
  simp only [mem_empty_iff_false, not_forall, iff_false, mem_pi, Classical.not_imp]
  exact ⟨i, hs, by simp [ht]⟩

Empty Component Implies Empty Product Set

Informal description

For an indexed family of sets $t_i \subseteq \alpha_i$ and an index set $s$, if there exists an index $i \in s$ such that $t_i = \emptyset$, then the product set $\prod_{i \in s} t_i$ is empty.

Set.univ_pi_eq_empty theorem

(ht : t i = ∅) : pi univ t = ∅

Full source

theorem univ_pi_eq_empty (ht : t i = ∅) : pi univ t = ∅ :=
  pi_eq_empty (mem_univ i) ht

Empty Component Implies Empty Universal Product Set

Informal description

For any family of sets $\{t_i\}_{i \in \iota}$ where $t_i \subseteq \alpha_i$, if there exists an index $i$ such that $t_i = \emptyset$, then the product set $\prod_{i \in \iota} t_i$ is empty.

Set.pi_nonempty_iff theorem

: (s.pi t).Nonempty ↔ ∀ i, ∃ x, i ∈ s → x ∈ t i

Full source

theorem pi_nonempty_iff : (s.pi t).Nonempty ↔ ∀ i, ∃ x, i ∈ s → x ∈ t i := by
  simp [Classical.skolem, Set.Nonempty]

Nonemptiness Criterion for Indexed Product of Sets

Informal description

For an index set $s$ and a family of sets $t_i \subseteq \alpha_i$ indexed by $i \in \iota$, the product set $\prod_{i \in s} t_i$ is nonempty if and only if for every index $i$, there exists an element $x \in \alpha_i$ such that whenever $i \in s$, then $x \in t_i$.

Set.univ_pi_nonempty_iff theorem

: (pi univ t).Nonempty ↔ ∀ i, (t i).Nonempty

Full source

theorem univ_pi_nonempty_iff : (pi univ t).Nonempty ↔ ∀ i, (t i).Nonempty := by
  simp [Classical.skolem, Set.Nonempty]

Nonemptiness of Universal Product Set

Informal description

The product set $\prod_{i} t_i$ over all indices is nonempty if and only if for every index $i$, the set $t_i$ is nonempty.

Set.pi_eq_empty_iff theorem

: s.pi t = ∅ ↔ ∃ i, IsEmpty (α i) ∨ i ∈ s ∧ t i = ∅

Full source

theorem pi_eq_empty_iff : s.pi t = ∅ ↔ ∃ i, IsEmpty (α i) ∨ i ∈ s ∧ t i = ∅ := by
  rw [← not_nonempty_iff_eq_empty, pi_nonempty_iff]
  push_neg
  refine exists_congr fun i => ?_
  cases isEmpty_or_nonempty (α i) <;> simp [*, forall_and, eq_empty_iff_forall_not_mem]

Empty Product Set Criterion: $\prod_{i \in s} t_i = \emptyset \leftrightarrow \exists i, (\text{IsEmpty } \alpha_i) \lor (i \in s \land t_i = \emptyset)$

Informal description

For an index set $s \subseteq \iota$ and a family of sets $t_i \subseteq \alpha_i$ for each $i \in \iota$, the product set $\prod_{i \in s} t_i$ is empty if and only if there exists an index $i$ such that either: 1. The type $\alpha_i$ is empty, or 2. $i \in s$ and the set $t_i$ is empty.

Set.univ_pi_eq_empty_iff theorem

: pi univ t = ∅ ↔ ∃ i, t i = ∅

Full source

@[simp]
theorem univ_pi_eq_empty_iff : pipi univ t = ∅ ↔ ∃ i, t i = ∅ := by
  simp [← not_nonempty_iff_eq_empty, univ_pi_nonempty_iff]

Empty Universal Product Set Criterion

Informal description

The product set $\prod_{i \in \iota} t_i$ is empty if and only if there exists an index $i \in \iota$ such that $t_i$ is empty.

Set.univ_pi_empty theorem

[h : Nonempty ι] : pi univ (fun _ => ∅ : ∀ i, Set (α i)) = ∅

Full source

@[simp]
theorem univ_pi_empty [h : Nonempty ι] : pi univ (fun _ => ∅ : ∀ i, Set (α i)) = ∅ :=
  univ_pi_eq_empty_iff.2 <| h.elim fun x => ⟨x, rfl⟩

Empty Product of Empty Sets over Nonempty Index Type

Informal description

For a nonempty index type $\iota$, the product set $\prod_{i \in \iota} \emptyset$ is empty.

Set.disjoint_univ_pi theorem

: Disjoint (pi univ t₁) (pi univ t₂) ↔ ∃ i, Disjoint (t₁ i) (t₂ i)

Full source

@[simp]
theorem disjoint_univ_pi : DisjointDisjoint (pi univ t₁) (pi univ t₂) ↔ ∃ i, Disjoint (t₁ i) (t₂ i) := by
  simp only [disjoint_iff_inter_eq_empty, ← pi_inter_distrib, univ_pi_eq_empty_iff]

Disjointness of Universal Product Sets

Informal description

For any family of sets $t_1$ and $t_2$ indexed by a type $\iota$, the universal product sets $\prod_{i \in \iota} t_1(i)$ and $\prod_{i \in \iota} t_2(i)$ are disjoint if and only if there exists an index $i \in \iota$ such that $t_1(i)$ and $t_2(i)$ are disjoint.

Set.Disjoint.set_pi theorem

(hi : i ∈ s) (ht : Disjoint (t₁ i) (t₂ i)) : Disjoint (s.pi t₁) (s.pi t₂)

Full source

theorem Disjoint.set_pi (hi : i ∈ s) (ht : Disjoint (t₁ i) (t₂ i)) : Disjoint (s.pi t₁) (s.pi t₂) :=
  disjoint_left.2 fun _ h₁ h₂ => disjoint_left.1 ht (h₁ _ hi) (h₂ _ hi)

Disjointness of Product Sets under Disjoint Components

Informal description

For any index $i$ in a set $s$, if the sets $t_1(i)$ and $t_2(i)$ are disjoint, then the product sets $\prod_{i \in s} t_1(i)$ and $\prod_{i \in s} t_2(i)$ are also disjoint.

Set.uniqueElim_preimage theorem

[Unique ι] (t : ∀ i, Set (α i)) : uniqueElim ⁻¹' pi univ t = t (default : ι)

Full source

theorem uniqueElim_preimage [Unique ι] (t : ∀ i, Set (α i)) :
    uniqueElimuniqueElim ⁻¹' pi univ t = t (default : ι) := by ext; simp [Unique.forall_iff]

Preimage of Universal Product Set under Unique Elimination

Informal description

For a unique type $\iota$ (a type with exactly one element) and a family of sets $t_i \subseteq \alpha_i$ indexed by $\iota$, the preimage of the universal product set $\prod_{i \in \iota} t_i$ under the unique elimination map $\mathrm{uniqueElim}$ is equal to the set $t_{\mathrm{default}}$ at the default index. That is, \[ \mathrm{uniqueElim}^{-1}\left(\prod_{i \in \iota} t_i\right) = t_{\mathrm{default}}. \]

Set.pi_eq_empty_iff' theorem

: s.pi t = ∅ ↔ ∃ i ∈ s, t i = ∅

Full source

theorem pi_eq_empty_iff' : s.pi t = ∅ ↔ ∃ i ∈ s, t i = ∅ := by simp [pi_eq_empty_iff]

Empty Product Set Criterion: $\prod_{i \in s} t_i = \emptyset \iff \exists i \in s, t_i = \emptyset$

Informal description

For a family of sets $t_i \subseteq \alpha_i$ indexed by $i \in s$, the product set $\prod_{i \in s} t_i$ is empty if and only if there exists some index $i \in s$ for which $t_i$ is empty. In other words: \[ \prod_{i \in s} t_i = \emptyset \iff \exists i \in s, t_i = \emptyset. \]

Set.disjoint_pi theorem

: Disjoint (s.pi t₁) (s.pi t₂) ↔ ∃ i ∈ s, Disjoint (t₁ i) (t₂ i)

Full source

@[simp]
theorem disjoint_pi : DisjointDisjoint (s.pi t₁) (s.pi t₂) ↔ ∃ i ∈ s, Disjoint (t₁ i) (t₂ i) := by
  simp only [disjoint_iff_inter_eq_empty, ← pi_inter_distrib, pi_eq_empty_iff']

Disjointness Criterion for Product Sets: $\prod_{i \in s} t_1(i) \cap \prod_{i \in s} t_2(i) = \emptyset \iff \exists i \in s, t_1(i) \cap t_2(i) = \emptyset$

Informal description

For any index set $s$ and any two families of sets $t_1$ and $t_2$ indexed by $s$, the product sets $\prod_{i \in s} t_1(i)$ and $\prod_{i \in s} t_2(i)$ are disjoint if and only if there exists some index $i \in s$ such that $t_1(i)$ and $t_2(i)$ are disjoint. In other words: \[ \prod_{i \in s} t_1(i) \cap \prod_{i \in s} t_2(i) = \emptyset \iff \exists i \in s, t_1(i) \cap t_2(i) = \emptyset. \]

Set.insert_pi theorem

(i : ι) (s : Set ι) (t : ∀ i, Set (α i)) : pi (insert i s) t = eval i ⁻¹' t i ∩ pi s t

Full source

@[simp]
theorem insert_pi (i : ι) (s : Set ι) (t : ∀ i, Set (α i)) :
    pi (insert i s) t = evaleval i ⁻¹' t ieval i ⁻¹' t i ∩ pi s t := by
  ext
  simp [pi, or_imp, forall_and]

Product Set Decomposition for Inserted Index: $\prod_{j \in s \cup \{i\}} t_j = \{f \mid f(i) \in t_i\} \cap \prod_{j \in s} t_j$

Informal description

For any index $i \in \iota$, any subset $s \subseteq \iota$, and any family of sets $t_j \subseteq \alpha_j$ for $j \in \iota$, the product set $\prod_{j \in s \cup \{i\}} t_j$ is equal to the intersection of the preimage of $t_i$ under the evaluation map at $i$ and the product set $\prod_{j \in s} t_j$. In other words: \[ \prod_{j \in s \cup \{i\}} t_j = \{f \mid f(i) \in t_i\} \cap \prod_{j \in s} t_j. \]

Set.singleton_pi theorem

(i : ι) (t : ∀ i, Set (α i)) : pi { i } t = eval i ⁻¹' t i

Full source

@[simp]
theorem singleton_pi (i : ι) (t : ∀ i, Set (α i)) : pi {i} t = evaleval i ⁻¹' t i := by
  ext
  simp [pi]

Product of Sets over Singleton Index Set Equals Preimage under Evaluation

Informal description

For any index $i$ in a type $\iota$ and any family of sets $t_i \subseteq \alpha_i$ indexed by $\iota$, the product set $\prod_{i \in \{i\}} t_i$ is equal to the preimage of $t_i$ under the evaluation function at $i$, i.e., $\{f \mid f(i) \in t_i\}$.

Set.singleton_pi' theorem

(i : ι) (t : ∀ i, Set (α i)) : pi { i } t = {x | x i ∈ t i}

Full source

theorem singleton_pi' (i : ι) (t : ∀ i, Set (α i)) : pi {i} t = { x | x i ∈ t i } :=
  singleton_pi i t

Product over Singleton Index Set Equals Evaluation Condition

Informal description

For any index $i$ in a type $\iota$ and any family of sets $t_i \subseteq \alpha_i$ indexed by $\iota$, the product set $\prod_{i \in \{i\}} t_i$ is equal to the set of all functions $x$ such that $x(i) \in t_i$.

Set.univ_pi_singleton theorem

(f : ∀ i, α i) : (pi univ fun i => {f i}) = ({ f } : Set (∀ i, α i))

Full source

theorem univ_pi_singleton (f : ∀ i, α i) : (pi univ fun i => {f i}) = ({f} : Set (∀ i, α i)) :=
  ext fun g => by simp [funext_iff]

Universal Product of Singletons Yields Singleton Function

Informal description

For any dependent function $f \in \prod_{i \in \iota} \alpha_i$, the product of singleton sets $\prod_{i \in \iota} \{f(i)\}$ over the universal set $\iota$ is equal to the singleton set $\{f\}$.

Set.preimage_pi theorem

 (s : Set ι) (t : ∀ i, Set (β i)) (f : ∀ i, α i → β i) :
  (fun (g : ∀ i, α i) i => f _ (g i)) ⁻¹' s.pi t = s.pi fun i => f i ⁻¹' t i

Full source

theorem preimage_pi (s : Set ι) (t : ∀ i, Set (β i)) (f : ∀ i, α i → β i) :
    (fun (g : ∀ i, α i) i => f _ (g i)) ⁻¹' s.pi t = s.pi fun i => f i ⁻¹' t i :=
  rfl

Preimage of Product Set under Componentwise Function Application

Informal description

Let $s \subseteq \iota$ be a subset of indices and for each $i \in \iota$, let $t_i \subseteq \beta_i$ be a subset. Given a family of functions $f_i : \alpha_i \to \beta_i$ for each $i \in \iota$, the preimage of the product set $\prod_{i \in s} t_i$ under the map $(g : \prod_{i \in \iota} \alpha_i) \mapsto (i \mapsto f_i(g(i)))$ is equal to the product set $\prod_{i \in s} (f_i^{-1}(t_i))$.

Set.pi_if theorem

 {p : ι → Prop} [h : DecidablePred p] (s : Set ι) (t₁ t₂ : ∀ i, Set (α i)) :
  (pi s fun i => if p i then t₁ i else t₂ i) = pi ({i ∈ s | p i}) t₁ ∩ pi ({i ∈ s | ¬p i}) t₂

Full source

theorem pi_if {p : ι → Prop} [h : DecidablePred p] (s : Set ι) (t₁ t₂ : ∀ i, Set (α i)) :
    (pi s fun i => if p i then t₁ i else t₂ i) =
      pipi ({ i ∈ s | p i }) t₁ ∩ pi ({ i ∈ s | ¬p i }) t₂ := by
  ext f
  refine ⟨fun h => ?_, ?_⟩
  · constructor <;>
      · rintro i ⟨his, hpi⟩
        simpa [*] using h i
  · rintro ⟨ht₁, ht₂⟩ i his
    by_cases p i <;> simp_all

Conditional Product Set Decomposition: $\prod_{i \in s} (p(i) \to t_1(i), \neg p(i) \to t_2(i)) = \prod_{i \in s \cap p} t_1(i) \cap \prod_{i \in s \cap \neg p} t_2(i)$

Informal description

Let $p : \iota \to \text{Prop}$ be a decidable predicate on an index set $\iota$, and let $s \subseteq \iota$ be a subset. For two families of sets $t_1, t_2 : \forall i, \text{Set } (\alpha_i)$, the product set $\prod_{i \in s} \text{if } p(i) \text{ then } t_1(i) \text{ else } t_2(i)$ is equal to the intersection of the product sets $\prod_{i \in \{i \in s \mid p(i)\}} t_1(i)$ and $\prod_{i \in \{i \in s \mid \neg p(i)\}} t_2(i)$.

Set.union_pi theorem

: (s₁ ∪ s₂).pi t = s₁.pi t ∩ s₂.pi t

Full source

theorem union_pi : (s₁ ∪ s₂).pi t = s₁.pi t ∩ s₂.pi t := by
  simp [pi, or_imp, forall_and, setOf_and]

Product Set over Union Equals Intersection of Product Sets

Informal description

For any two sets $s_1, s_2 \subseteq \iota$ and a family of sets $t_i \subseteq \alpha_i$ for each $i \in \iota$, the product set $\prod_{i \in s_1 \cup s_2} t_i$ is equal to the intersection of the product sets $\prod_{i \in s_1} t_i$ and $\prod_{i \in s_2} t_i$.

Set.union_pi_inter theorem

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

Full source

theorem union_pi_inter
    (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₂ := by
  ext x
  simp only [mem_pi, mem_union, mem_inter_iff]
  refine ⟨fun h ↦ ⟨fun i his₁ ↦ (h i (Or.inl his₁)).1, fun i his₂ ↦ (h i (Or.inr his₂)).2⟩,
    fun h i hi ↦ ?_⟩
  rcases hi with hi | hi
  · by_cases hi2 : i ∈ s₂
    · exact ⟨h.1 i hi, h.2 i hi2⟩
    · refine ⟨h.1 i hi, ?_⟩
      rw [ht₂ i hi2]
      exact mem_univ _
  · by_cases hi1 : i ∈ s₁
    · exact ⟨h.1 i hi1, h.2 i hi⟩
    · refine ⟨?_, h.2 i hi⟩
      rw [ht₁ i hi1]
      exact mem_univ _

Product of Intersections over Union Equals Intersection of Products

Informal description

Let $s_1$ and $s_2$ be subsets of an index set $\iota$, and let $t_1$ and $t_2$ be families of sets over $\alpha_i$ for each $i \in \iota$. Suppose that for all $i \notin s_1$, $t_1(i) = \text{univ}$ (the universal set), and similarly for all $i \notin s_2$, $t_2(i) = \text{univ}$. Then the product of the sets $(t_1(i) \cap t_2(i))$ over the union $s_1 \cup s_2$ is equal to the intersection of the product of $t_1$ over $s_1$ and the product of $t_2$ over $s_2$: \[ \prod_{i \in s_1 \cup s_2} (t_1(i) \cap t_2(i)) = \left(\prod_{i \in s_1} t_1(i)\right) \cap \left(\prod_{i \in s_2} t_2(i)\right). \]

Set.pi_inter_compl theorem

(s : Set ι) : pi s t ∩ pi sᶜ t = pi univ t

Full source

@[simp]
theorem pi_inter_compl (s : Set ι) : pipi s t ∩ pi sᶜ t = pi univ t := by
  rw [← union_pi, union_compl_self]

Intersection of Product Sets with Complement Equals Full Product Set

Informal description

For any subset $s$ of an index set $\iota$ and any family of sets $t_i \subseteq \alpha_i$ for $i \in \iota$, the intersection of the product sets $\prod_{i \in s} t_i$ and $\prod_{i \in s^c} t_i$ is equal to the product set $\prod_{i \in \iota} t_i$, where $s^c$ denotes the complement of $s$ in $\iota$. In symbols: \[ \left(\prod_{i \in s} t_i\right) \cap \left(\prod_{i \in \iota \setminus s} t_i\right) = \prod_{i \in \iota} t_i. \]

Set.pi_update_of_not_mem theorem

 [DecidableEq ι] (hi : i ∉ s) (f : ∀ j, α j) (a : α i) (t : ∀ j, α j → Set (β j)) :
  (s.pi fun j => t j (update f i a j)) = s.pi fun j => t j (f j)

Full source

theorem pi_update_of_not_mem [DecidableEq ι] (hi : i ∉ s) (f : ∀ j, α j) (a : α i)
    (t : ∀ j, α j → Set (β j)) : (s.pi fun j => t j (update f i a j)) = s.pi fun j => t j (f j) :=
  (pi_congr rfl) fun j hj => by
    rw [update_of_ne]
    exact fun h => hi (h ▸ hj)

Invariance of Product Set under Update Outside Index Set

Informal description

Let $\iota$ be a type with decidable equality, $s \subseteq \iota$ a subset, and $i \in \iota$ an index not in $s$. For any function $f \in \prod_{j \in \iota} \alpha_j$, any element $a \in \alpha_i$, and any family of sets $t_j \subseteq \beta_j$ depending on $\alpha_j$, the product set $\prod_{j \in s} t_j(\text{update } f \, i \, a \, j)$ is equal to $\prod_{j \in s} t_j(f(j))$. Here, $\text{update } f \, i \, a$ denotes the function that coincides with $f$ everywhere except at $i$, where it takes the value $a$.

Set.pi_update_of_mem theorem

 [DecidableEq ι] (hi : i ∈ s) (f : ∀ j, α j) (a : α i) (t : ∀ j, α j → Set (β j)) :
  (s.pi fun j => t j (update f i a j)) = {x | x i ∈ t i a} ∩ (s \ { i }).pi fun j => t j (f j)

Full source

theorem pi_update_of_mem [DecidableEq ι] (hi : i ∈ s) (f : ∀ j, α j) (a : α i)
    (t : ∀ j, α j → Set (β j)) :
    (s.pi fun j => t j (update f i a j)) = { x | x i ∈ t i a }{ x | x i ∈ t i a } ∩ (s \ {i}).pi fun j => t j (f j) :=
  calc
    (s.pi fun j => t j (update f i a j)) = ({i}{i} ∪ s \ {i}).pi fun j => t j (update f i a j) := by
        rw [union_diff_self, union_eq_self_of_subset_left (singleton_subset_iff.2 hi)]
    _ = { x | x i ∈ t i a }{ x | x i ∈ t i a } ∩ (s \ {i}).pi fun j => t j (f j) := by
        rw [union_pi, singleton_pi', update_self, pi_update_of_not_mem]; simp

Product Set under Update at Index in Subset

Informal description

Let $\iota$ be a type with decidable equality, $s \subseteq \iota$ a subset, and $i \in \iota$ an index in $s$. For any function $f \in \prod_{j \in \iota} \alpha_j$, any element $a \in \alpha_i$, and any family of sets $t_j \subseteq \beta_j$ depending on $\alpha_j$, the product set $\prod_{j \in s} t_j(\text{update } f \, i \, a \, j)$ is equal to the intersection of the set $\{x \mid x_i \in t_i(a)\}$ with the product set $\prod_{j \in s \setminus \{i\}} t_j(f(j))$. Here, $\text{update } f \, i \, a$ denotes the function that coincides with $f$ everywhere except at $i$, where it takes the value $a$.

Set.univ_pi_update theorem

 [DecidableEq ι] {β : ι → Type*} (i : ι) (f : ∀ j, α j) (a : α i) (t : ∀ j, α j → Set (β j)) :
  (pi univ fun j => t j (update f i a j)) = {x | x i ∈ t i a} ∩ pi { i }ᶜ fun j => t j (f j)

Full source

theorem univ_pi_update [DecidableEq ι] {β : ι → Type*} (i : ι) (f : ∀ j, α j) (a : α i)
    (t : ∀ j, α j → Set (β j)) :
    (pi univ fun j => t j (update f i a j)) = { x | x i ∈ t i a }{ x | x i ∈ t i a } ∩ pi {i}ᶜ fun j => t j (f j) := by
  rw [compl_eq_univ_diff, ← pi_update_of_mem (mem_univ _)]

Universal Product Set under Update at Index Equals Intersection of Component and Complement Product

Informal description

Let $\iota$ be a type with decidable equality, and let $\beta : \iota \to \text{Type}$ be a family of types. For any index $i \in \iota$, any function $f \in \prod_{j \in \iota} \alpha_j$, any element $a \in \alpha_i$, and any family of sets $t_j \subseteq \beta_j$ depending on $\alpha_j$, the product set $\prod_{j \in \text{univ}} t_j(\text{update } f \, i \, a \, j)$ is equal to the intersection of the set $\{x \mid x_i \in t_i(a)\}$ with the product set $\prod_{j \in \{i\}^c} t_j(f(j))$. Here, $\text{update } f \, i \, a$ denotes the function that coincides with $f$ everywhere except at $i$, where it takes the value $a$, and $\{i\}^c$ denotes the complement of the singleton set $\{i\}$ in $\iota$.

Set.univ_pi_update_univ theorem

[DecidableEq ι] (i : ι) (s : Set (α i)) : pi univ (update (fun j : ι => (univ : Set (α j))) i s) = eval i ⁻¹' s

Full source

theorem univ_pi_update_univ [DecidableEq ι] (i : ι) (s : Set (α i)) :
    pi univ (update (fun j : ι => (univ : Set (α j))) i s) = evaleval i ⁻¹' s := by
  rw [univ_pi_update i (fun j => (univ : Set (α j))) s fun j t => t, pi_univ, inter_univ, preimage]

Universal Product Set with Single Component Update Equals Evaluation Preimage

Informal description

Let $\iota$ be a type with decidable equality and $\alpha : \iota \to \text{Type}$ a family of types. For any index $i \in \iota$ and any subset $s \subseteq \alpha_i$, the product set $\prod_{j \in \iota} t_j$, where $t_j = \alpha_j$ for all $j \neq i$ and $t_i = s$, is equal to the preimage of $s$ under the evaluation function at $i$. That is, \[ \prod_{j \in \iota} t_j = \text{eval}_i^{-1}(s), \] where $t_j = \begin{cases} s & \text{if } j = i, \\ \alpha_j & \text{otherwise.} \end{cases}$

Set.eval_image_pi_subset theorem

(hs : i ∈ s) : eval i '' s.pi t ⊆ t i

Full source

theorem eval_image_pi_subset (hs : i ∈ s) : evaleval i '' s.pi teval i '' s.pi t ⊆ t i :=
  image_subset_iff.2 fun _ hf => hf i hs

Evaluation Image of Product Set is Subset of Component

Informal description

For any index $i$ in the index set $s$, the image of the product set $\prod_{j \in s} t_j$ under the evaluation function at $i$ is a subset of $t_i$. In symbols: \[ \text{eval}_i\left(\prod_{j \in s} t_j\right) \subseteq t_i. \]

Set.eval_image_univ_pi_subset theorem

: eval i '' pi univ t ⊆ t i

Full source

theorem eval_image_univ_pi_subset : evaleval i '' pi univ teval i '' pi univ t ⊆ t i :=
  eval_image_pi_subset (mem_univ i)

Evaluation Image of Universal Product Set is Subset of Component

Informal description

For any index $i$ and any family of sets $t_i \subseteq \alpha_i$, the image of the universal product set $\prod_{j} t_j$ under the evaluation function at $i$ is a subset of $t_i$. In symbols: \[ \text{eval}_i\left(\prod_{j} t_j\right) \subseteq t_i. \]

Set.subset_eval_image_pi theorem

(ht : (s.pi t).Nonempty) (i : ι) : t i ⊆ eval i '' s.pi t

Full source

theorem subset_eval_image_pi (ht : (s.pi t).Nonempty) (i : ι) : t i ⊆ eval i '' s.pi t := by
  classical
  obtain ⟨f, hf⟩ := ht
  refine fun y hy => ⟨update f i y, fun j hj => ?_, update_self ..⟩
  obtain rfl | hji := eq_or_ne j i <;> simp [*, hf _ hj]

Inclusion of Component Set in Evaluation Image of Product Set

Informal description

For any nonempty product set $\prod_{i \in s} t_i$ and any index $i \in \iota$, the set $t_i$ is a subset of the image of the evaluation function at $i$ applied to the product set. In other words, every element of $t_i$ is the evaluation at $i$ of some function in $\prod_{i \in s} t_i$.

Set.eval_image_pi theorem

(hs : i ∈ s) (ht : (s.pi t).Nonempty) : eval i '' s.pi t = t i

Full source

theorem eval_image_pi (hs : i ∈ s) (ht : (s.pi t).Nonempty) : evaleval i '' s.pi t = t i :=
  (eval_image_pi_subset hs).antisymm (subset_eval_image_pi ht i)

Equality of Evaluation Image and Component Set for Nonempty Product

Informal description

For any index $i$ in the index set $s$ and any nonempty product set $\prod_{i \in s} t_i$, the image of the evaluation function at $i$ applied to the product set equals $t_i$. In symbols: \[ \text{eval}_i\left(\prod_{j \in s} t_j\right) = t_i. \]

Set.eval_image_pi_of_not_mem theorem

[Decidable (s.pi t).Nonempty] (hi : i ∉ s) : eval i '' s.pi t = if (s.pi t).Nonempty then univ else ∅

Full source

lemma eval_image_pi_of_not_mem [Decidable (s.pi t).Nonempty] (hi : i ∉ s) :
    evaleval i '' s.pi t = if (s.pi t).Nonempty then univ else ∅ := by
  classical
  ext xᵢ
  simp only [eval, mem_image, mem_pi, Set.Nonempty, mem_ite_empty_right, mem_univ, and_true]
  constructor
  · rintro ⟨x, hx, rfl⟩
    exact ⟨x, hx⟩
  · rintro ⟨x, hx⟩
    refine ⟨Function.update x i xᵢ, ?_⟩
    simpa (config := { contextual := true }) [(ne_of_mem_of_not_mem · hi)]

Image of Evaluation on Product Set for Non-Member Index

Informal description

For any index $i$ not in the index set $s$ (i.e., $i \notin s$), the image of the evaluation function at $i$ applied to the product set $\prod_{i \in s} t_i$ is equal to the universal set if the product set is nonempty, and the empty set otherwise. In other words: \[ \text{eval}_i \left( \prod_{i \in s} t_i \right) = \begin{cases} \text{univ} & \text{if } \prod_{i \in s} t_i \text{ is nonempty}, \\ \emptyset & \text{otherwise.} \end{cases} \]

Set.eval_image_univ_pi theorem

(ht : (pi univ t).Nonempty) : (fun f : ∀ i, α i => f i) '' pi univ t = t i

Full source

@[simp]
theorem eval_image_univ_pi (ht : (pi univ t).Nonempty) :
    (fun f : ∀ i, α i => f i) '' pi univ t = t i :=
  eval_image_pi (mem_univ i) ht

Evaluation Image of Universal Product Set Equals Component Set

Informal description

For any index $i$ and any nonempty product set $\prod_{i \in \text{univ}} t_i$ (where $\text{univ}$ denotes the universal set of indices), the image of the evaluation function at $i$ applied to the product set equals $t_i$. In symbols: \[ \text{eval}_i\left(\prod_{j \in \text{univ}} t_j\right) = t_i. \]

Set.piMap_mapsTo_pi theorem

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

Full source

theorem piMap_mapsTo_pi {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) :=
  fun _x hx i hi => h i hi (hx i hi)

Component-wise Function Maps Product Set into Product Set

Informal description

Let $I$ be a set of indices, and for each $i \in I$, let $f_i : \alpha_i \to \beta_i$ be a function, $s_i \subseteq \alpha_i$ and $t_i \subseteq \beta_i$ be sets. If for every $i \in I$, the function $f_i$ maps $s_i$ into $t_i$ (i.e., $f_i(s_i) \subseteq t_i$), then the component-wise application $\text{Pi.map}\, f$ maps the product set $\prod_{i \in I} s_i$ into the product set $\prod_{i \in I} t_i$.

Set.piMap_image_pi_subset theorem

{f : ∀ i, α i → β i} (t : ∀ i, Set (α i)) : Pi.map f '' s.pi t ⊆ s.pi fun i ↦ f i '' t i

Full source

theorem piMap_image_pi_subset {f : ∀ i, α i → β i} (t : ∀ i, Set (α i)) :
    Pi.mapPi.map f '' s.pi tPi.map f '' s.pi t ⊆ s.pi fun i ↦ f i '' t i :=
  image_subset_iff.2 <| piMap_mapsTo_pi fun _ _ => mapsTo_image _ _

Image of Product Set under Component-wise Map is Subset of Product of Images

Informal description

Let $s$ be a set of indices, and for each $i \in s$, let $t_i \subseteq \alpha_i$ be a set and $f_i : \alpha_i \to \beta_i$ be a function. Then the image of the product set $\prod_{i \in s} t_i$ under the component-wise application $\text{Pi.map}\, f$ is contained in the product set $\prod_{i \in s} f_i(t_i)$. In symbols: \[ \text{Pi.map}\, f \left( \prod_{i \in s} t_i \right) \subseteq \prod_{i \in s} f_i(t_i). \]

Set.piMap_image_pi theorem

 {f : ∀ i, α i → β i} (hf : ∀ i ∉ s, Surjective (f i)) (t : ∀ i, Set (α i)) :
  Pi.map f '' s.pi t = s.pi fun i ↦ f i '' t i

Full source

theorem piMap_image_pi {f : ∀ i, α i → β i} (hf : ∀ i ∉ s, Surjective (f i)) (t : ∀ i, Set (α i)) :
    Pi.mapPi.map f '' s.pi t = s.pi fun i ↦ f i '' t i := by
  refine Subset.antisymm (piMap_image_pi_subset _) fun b hb => ?_
  have (i : ι) : ∃ a, f i a = b i ∧ (i ∈ s → a ∈ t i) := by
    if hi : i ∈ s then
      exact (hb i hi).imp fun a ⟨hat, hab⟩ ↦ ⟨hab, fun _ ↦ hat⟩
    else
      exact (hf i hi (b i)).imp fun a ha ↦ ⟨ha, (absurd · hi)⟩
  choose a hab hat using this
  exact ⟨a, hat, funext hab⟩

Equality of Image of Product Set and Product of Images under Component-wise Map with Surjectivity Condition

Informal description

Let $s$ be a set of indices, and for each $i \in s$, let $t_i \subseteq \alpha_i$ be a set and $f_i : \alpha_i \to \beta_i$ be a function. If for every index $i \notin s$, the function $f_i$ is surjective, then the image of the product set $\prod_{i \in s} t_i$ under the component-wise application $\text{Pi.map}\, f$ is equal to the product set $\prod_{i \in s} f_i(t_i)$. In symbols: \[ \text{Pi.map}\, f \left( \prod_{i \in s} t_i \right) = \prod_{i \in s} f_i(t_i). \]

Set.piMap_image_univ_pi theorem

(f : ∀ i, α i → β i) (t : ∀ i, Set (α i)) : Pi.map f '' univ.pi t = univ.pi fun i ↦ f i '' t i

Full source

theorem piMap_image_univ_pi (f : ∀ i, α i → β i) (t : ∀ i, Set (α i)) :
    Pi.mapPi.map f '' univ.pi t = univ.pi fun i ↦ f i '' t i :=
  piMap_image_pi (by simp) t

Image of Universal Product Set under Component-wise Map Equals Product of Images

Informal description

For a family of functions $f_i : \alpha_i \to \beta_i$ indexed by $i \in \iota$ and a family of sets $t_i \subseteq \alpha_i$, the image of the product set $\prod_{i \in \iota} t_i$ under the component-wise mapping $\text{Pi.map}\, f$ is equal to the product set $\prod_{i \in \iota} f_i(t_i)$. In symbols: \[ \text{Pi.map}\, f \left( \prod_{i \in \iota} t_i \right) = \prod_{i \in \iota} f_i(t_i). \]

Set.range_piMap theorem

(f : ∀ i, α i → β i) : range (Pi.map f) = pi univ fun i ↦ range (f i)

Full source

@[simp]
theorem range_piMap (f : ∀ i, α i → β i) : range (Pi.map f) = pi univ fun i ↦ range (f i) := by
  simp only [← image_univ, ← piMap_image_univ_pi, pi_univ]

Range of Component-wise Mapping Equals Product of Ranges

Informal description

For a family of functions $f_i : \alpha_i \to \beta_i$ indexed by $i \in \iota$, the range of the component-wise mapping function $\text{Pi.map} \, f$ is equal to the product of the ranges of the individual functions $f_i$ over the universal index set. That is, \[ \text{range} (\text{Pi.map} \, f) = \prod_{i \in \iota} \text{range} (f_i). \]

Set.pi_subset_pi_iff theorem

: pi s t₁ ⊆ pi s t₂ ↔ (∀ i ∈ s, t₁ i ⊆ t₂ i) ∨ pi s t₁ = ∅

Full source

theorem pi_subset_pi_iff : pipi s t₁ ⊆ pi s t₂pi s t₁ ⊆ pi s t₂ ↔ (∀ i ∈ s, t₁ i ⊆ t₂ i) ∨ pi s t₁ = ∅ := by
  refine
    ⟨fun h => or_iff_not_imp_right.2 ?_, fun h => h.elim pi_mono fun h' => h'.symm ▸ empty_subset _⟩
  rw [← Ne, ← nonempty_iff_ne_empty]
  intro hne i hi
  simpa only [eval_image_pi hi hne, eval_image_pi hi (hne.mono h)] using
    image_subset (fun f : ∀ i, α i => f i) h

Product Set Subset Criterion: $\prod_{i \in s} t₁_i \subseteq \prod_{i \in s} t₂_i \iff (\forall i \in s, t₁_i \subseteq t₂_i) \lor \prod_{i \in s} t₁_i = \emptyset$

Informal description

For any index set $s$ and any two families of sets $(t_1(i))_{i \in s}$ and $(t_2(i))_{i \in s}$, the product set $\prod_{i \in s} t_1(i)$ is a subset of $\prod_{i \in s} t_2(i)$ if and only if either: 1. For every $i \in s$, $t_1(i) \subseteq t_2(i)$, or 2. The product set $\prod_{i \in s} t_1(i)$ is empty.

Set.univ_pi_subset_univ_pi_iff theorem

: pi univ t₁ ⊆ pi univ t₂ ↔ (∀ i, t₁ i ⊆ t₂ i) ∨ ∃ i, t₁ i = ∅

Full source

theorem univ_pi_subset_univ_pi_iff :
    pipi univ t₁ ⊆ pi univ t₂pi univ t₁ ⊆ pi univ t₂ ↔ (∀ i, t₁ i ⊆ t₂ i) ∨ ∃ i, t₁ i = ∅ := by simp [pi_subset_pi_iff]

Universal Product Subset Criterion: $\prod_{i} t₁_i \subseteq \prod_{i} t₂_i \iff (\forall i, t₁_i \subseteq t₂_i) \lor (\exists i, t₁_i = \emptyset)$

Informal description

For any family of sets $(t₁_i)_{i \in \iota}$ and $(t₂_i)_{i \in \iota}$ indexed by a type $\iota$, the product $\prod_{i \in \iota} t₁_i$ is a subset of $\prod_{i \in \iota} t₂_i$ if and only if either: 1. For every index $i \in \iota$, the set $t₁_i$ is a subset of $t₂_i$, or 2. There exists some index $i \in \iota$ for which $t₁_i$ is the empty set.

Set.eval_preimage theorem

[DecidableEq ι] {s : Set (α i)} : eval i ⁻¹' s = pi univ (update (fun _ => univ) i s)

Full source

theorem eval_preimage [DecidableEq ι] {s : Set (α i)} :
    evaleval i ⁻¹' s = pi univ (update (fun _ => univ) i s) := by
  ext x
  simp [@forall_update_iff _ (fun i => Set (α i)) _ _ _ _ fun i' y => x i' ∈ y]

Preimage of Evaluation Function Equals Product Set with Updated Component

Informal description

Let $\iota$ be a type with decidable equality and let $s$ be a subset of $\alpha_i$ for some fixed $i \in \iota$. The preimage of $s$ under the evaluation function $\mathrm{eval}_i$ (which evaluates a dependent function at index $i$) is equal to the product set $\prod_{j \in \iota} t_j$, where $t_j = \alpha_j$ for all $j \neq i$ and $t_i = s$. In other words, for any $s \subseteq \alpha_i$, we have: \[ \mathrm{eval}_i^{-1}(s) = \prod_{j \in \iota} t_j \quad \text{where} \quad t_j = \begin{cases} s & \text{if } j = i, \\ \alpha_j & \text{otherwise.} \end{cases} \]

Set.eval_preimage' theorem

[DecidableEq ι] {s : Set (α i)} : eval i ⁻¹' s = pi { i } (update (fun _ => univ) i s)

Full source

theorem eval_preimage' [DecidableEq ι] {s : Set (α i)} :
    evaleval i ⁻¹' s = pi {i} (update (fun _ => univ) i s) := by
  ext
  simp

Preimage under Evaluation Equals Singleton Product with Updated Component

Informal description

Let $\iota$ be a type with decidable equality and let $s$ be a subset of $\alpha_i$ for some fixed $i \in \iota$. The preimage of $s$ under the evaluation function $\mathrm{eval}_i$ (which evaluates a dependent function at index $i$) is equal to the product set $\prod_{j \in \{i\}} t_j$, where $t_j = \alpha_j$ for all $j \neq i$ and $t_i = s$. In other words, for any $s \subseteq \alpha_i$, we have: \[ \mathrm{eval}_i^{-1}(s) = \prod_{j \in \{i\}} t_j \quad \text{where} \quad t_j = \begin{cases} s & \text{if } j = i, \\ \alpha_j & \text{otherwise.} \end{cases} \]

Set.update_preimage_pi theorem

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

Full source

theorem update_preimage_pi [DecidableEq ι] {f : ∀ i, α i} (hi : i ∈ s)
    (hf : ∀ j ∈ s, j ≠ i → f j ∈ t j) : updateupdate f i ⁻¹' s.pi t = t i := by
  ext x
  refine ⟨fun h => ?_, fun hx j hj => ?_⟩
  · convert h i hi
    simp
  · obtain rfl | h := eq_or_ne j i
    · simpa
    · rw [update_of_ne h]
      exact hf j hj h

Preimage of Product Set under Function Update Equals Component Set

Informal description

Let $\iota$ be a type with decidable equality, and let $s \subseteq \iota$ be a subset. Given a dependent function $f : \prod_{i \in \iota} \alpha_i$ and a family of sets $t_i \subseteq \alpha_i$ for each $i \in \iota$, suppose that $i \in s$ and for all $j \in s$ with $j \neq i$, we have $f(j) \in t(j)$. Then the preimage of the product set $\prod_{i \in s} t_i$ under the function update operation $\text{update}\,f\,i$ is equal to $t(i)$. In other words, \[ (\text{update}\,f\,i)^{-1}\left(\prod_{i \in s} t_i\right) = t(i). \]

Set.update_image theorem

 [DecidableEq ι] (x : (i : ι) → β i) (i : ι) (s : Set (β i)) :
  update x i '' s = Set.univ.pi (update (fun j ↦ {x j}) i s)

Full source

theorem update_image [DecidableEq ι] (x : (i : ι) → β i) (i : ι) (s : Set (β i)) :
    updateupdate x i '' s = Set.univ.pi (update (fun j ↦ {x j}) i s) := by
  ext y
  simp only [mem_image, update_eq_iff, ne_eq, and_left_comm (a := _ ∈ s), exists_eq_left, mem_pi,
    mem_univ, true_implies]
  rw [forall_update_iff (p := fun x s => y x ∈ s)]
  simp [eq_comm]

Image of Function Update Equals Universal Product of Singletons with Updated Component

Informal description

Let $\iota$ be a type with decidable equality, $\beta$ a family of types indexed by $\iota$, $x : \prod_{i \in \iota} \beta_i$ a dependent function, $i \in \iota$ an index, and $s \subseteq \beta_i$ a subset. Then the image of $s$ under the function update operation $\text{update}\,x\,i$ is equal to the product of the universal set $\prod_{j \in \iota} \alpha_j$ where $\alpha_j = \{x_j\}$ for all $j \neq i$ and $\alpha_i = s$. That is, \[ \text{update}\,x\,i\,''s = \prod_{j \in \iota} \alpha_j \] where $\alpha_j = \begin{cases} s & \text{if } j = i, \\ \{x_j\} & \text{otherwise.} \end{cases}$

Set.update_preimage_univ_pi theorem

[DecidableEq ι] {f : ∀ i, α i} (hf : ∀ j ≠ i, f j ∈ t j) : update f i ⁻¹' pi univ t = t i

Full source

theorem update_preimage_univ_pi [DecidableEq ι] {f : ∀ i, α i} (hf : ∀ j ≠ i, f j ∈ t j) :
    updateupdate f i ⁻¹' pi univ t = t i :=
  update_preimage_pi (mem_univ i) fun j _ => hf j

Preimage of Universal Product Set under Function Update Equals Component Set

Informal description

Let $\iota$ be a type with decidable equality, and let $f : \prod_{i \in \iota} \alpha_i$ be a dependent function. Suppose that for all $j \neq i$, $f(j) \in t(j)$. Then the preimage of the universal product set $\prod_{i \in \iota} t_i$ under the function update operation $\text{update}\,f\,i$ is equal to $t(i)$. In other words, \[ (\text{update}\,f\,i)^{-1}\left(\prod_{i \in \iota} t_i\right) = t(i). \]

Set.subset_pi_eval_image theorem

(s : Set ι) (u : Set (∀ i, α i)) : u ⊆ pi s fun i => eval i '' u

Full source

theorem subset_pi_eval_image (s : Set ι) (u : Set (∀ i, α i)) : u ⊆ pi s fun i => eval i '' u :=
  fun f hf _ _ => ⟨f, hf, rfl⟩

Inclusion of Function Set in Product of Evaluation Images

Informal description

For any index set $s \subseteq \iota$ and any set $u$ of dependent functions in $\prod_{i \in \iota} \alpha_i$, the set $u$ is contained in the product $\prod_{i \in s} \text{eval}_i \,'' u$, where $\text{eval}_i \,'' u$ denotes the image of $u$ under evaluation at index $i$. In other words, every function $f \in u$ satisfies $f(i) \in \text{eval}_i \,'' u$ for all $i \in s$.

Set.univ_pi_ite theorem

 (s : Set ι) [DecidablePred (· ∈ s)] (t : ∀ i, Set (α i)) : (pi univ fun i => if i ∈ s then t i else univ) = s.pi t

Full source

theorem univ_pi_ite (s : Set ι) [DecidablePred (· ∈ s)] (t : ∀ i, Set (α i)) :
    (pi univ fun i => if i ∈ s then t i else univ) = s.pi t := by
  ext
  simp_rw [mem_univ_pi]
  refine forall_congr' fun i => ?_
  split_ifs with h <;> simp [h]

Universal Product of Conditional Sets Equals Product over Subset

Informal description

For any set $s \subseteq \iota$ with a decidable membership predicate and any family of sets $t_i \subseteq \alpha_i$ for $i \in \iota$, the product of sets defined by: \[ \prod_{i \in \iota} \begin{cases} t_i & \text{if } i \in s \\ \alpha_i & \text{otherwise} \end{cases} \] is equal to the product of the sets $t_i$ over $i \in s$, i.e., $\prod_{i \in s} t_i$.

Equiv.piCongrLeft_symm_preimage_pi theorem

 (f : ι' ≃ ι) (s : Set ι') (t : ∀ i, Set (α i)) : (f.piCongrLeft α).symm ⁻¹' s.pi (fun i' => t <| f i') = (f '' s).pi t

Full source

theorem piCongrLeft_symm_preimage_pi (f : ι' ≃ ι) (s : Set ι') (t : ∀ i, Set (α i)) :
    (f.piCongrLeft α).symm ⁻¹' s.pi (fun i' => t <| f i') = (f '' s).pi t := by
  ext; simp

Preimage of Product Set under Inverse Equivalence is Product over Image

Informal description

Let $f : \iota' \simeq \iota$ be an equivalence between index types $\iota'$ and $\iota$, $s \subseteq \iota'$ be a subset of $\iota'$, and $t_i \subseteq \alpha_i$ be a family of subsets indexed by $i \in \iota$. Then the preimage under the inverse of the equivalence $\text{piCongrLeft}_f(\alpha)$ of the product set $\prod_{i' \in s} t_{f(i')}$ is equal to the product set $\prod_{i \in f(s)} t_i$. In symbols: $$(\text{piCongrLeft}_f(\alpha))^{-1} \left( \prod_{i' \in s} t_{f(i')} \right) = \prod_{i \in f(s)} t_i$$

Equiv.piCongrLeft_symm_preimage_univ_pi theorem

(f : ι' ≃ ι) (t : ∀ i, Set (α i)) : (f.piCongrLeft α).symm ⁻¹' univ.pi (fun i' => t <| f i') = univ.pi t

Full source

theorem piCongrLeft_symm_preimage_univ_pi (f : ι' ≃ ι) (t : ∀ i, Set (α i)) :
    (f.piCongrLeft α).symm ⁻¹' univ.pi (fun i' => t <| f i') = univ.pi t := by
  simpa [f.surjective.range_eq] using piCongrLeft_symm_preimage_pi f univ t

Preimage of Universal Product Set under Inverse Equivalence Equals Universal Product Set

Informal description

Let $f : \iota' \simeq \iota$ be an equivalence between index types $\iota'$ and $\iota$, and let $t_i \subseteq \alpha_i$ be a family of subsets indexed by $i \in \iota$. Then the preimage under the inverse of the equivalence $\text{piCongrLeft}_f(\alpha)$ of the universal product set $\prod_{i' \in \iota'} t_{f(i')}$ is equal to the universal product set $\prod_{i \in \iota} t_i$. In symbols: $$(\text{piCongrLeft}_f(\alpha))^{-1} \left( \prod_{i' \in \iota'} t_{f(i')} \right) = \prod_{i \in \iota} t_i$$

Equiv.piCongrLeft_preimage_pi theorem

(f : ι' ≃ ι) (s : Set ι') (t : ∀ i, Set (α i)) : f.piCongrLeft α ⁻¹' (f '' s).pi t = s.pi fun i => t (f i)

Full source

theorem piCongrLeft_preimage_pi (f : ι' ≃ ι) (s : Set ι') (t : ∀ i, Set (α i)) :
    f.piCongrLeft α ⁻¹' (f '' s).pi t = s.pi fun i => t (f i) := by
  apply Set.ext
  rw [← (f.piCongrLeft α).symm.forall_congr_right]
  simp

Preimage of Product Set under Equivalence is Product over Preimage Indices

Informal description

Let $f : \iota' \simeq \iota$ be an equivalence between index types $\iota'$ and $\iota$, $s \subseteq \iota'$ be a subset of $\iota'$, and $t_i \subseteq \alpha_i$ be a family of subsets indexed by $i \in \iota$. Then the preimage under the equivalence $\text{piCongrLeft}_f(\alpha)$ of the product set $\prod_{i \in f(s)} t_i$ is equal to the product set $\prod_{i' \in s} t_{f(i')}$. In symbols: $$(\text{piCongrLeft}_f(\alpha))^{-1}\left(\prod_{i \in f(s)} t_i\right) = \prod_{i' \in s} t_{f(i')}$$

Equiv.piCongrLeft_preimage_univ_pi theorem

(f : ι' ≃ ι) (t : ∀ i, Set (α i)) : f.piCongrLeft α ⁻¹' univ.pi t = univ.pi fun i => t (f i)

Full source

theorem piCongrLeft_preimage_univ_pi (f : ι' ≃ ι) (t : ∀ i, Set (α i)) :
    f.piCongrLeft α ⁻¹' univ.pi t = univ.pi fun i => t (f i) := by
  simpa [f.surjective.range_eq] using piCongrLeft_preimage_pi f univ t

Preimage of Universal Product Set under Index Equivalence

Informal description

Let $f : \iota' \simeq \iota$ be an equivalence between index types $\iota'$ and $\iota$, and let $t_i \subseteq \alpha_i$ be a family of subsets indexed by $i \in \iota$. Then the preimage under the equivalence $\text{piCongrLeft}_f(\alpha)$ of the universal product set $\prod_{i \in \iota} t_i$ is equal to the universal product set $\prod_{i' \in \iota'} t_{f(i')}$. In symbols: $$(\text{piCongrLeft}_f(\alpha))^{-1}\left(\prod_{i \in \iota} t_i\right) = \prod_{i' \in \iota'} t_{f(i')}$$

Equiv.sumPiEquivProdPi_symm_preimage_univ_pi theorem

 (π : ι ⊕ ι' → Type*) (t : ∀ i, Set (π i)) :
  (sumPiEquivProdPi π).symm ⁻¹' univ.pi t = univ.pi (fun i => t (.inl i)) ×ˢ univ.pi fun i => t (.inr i)

Full source

theorem sumPiEquivProdPi_symm_preimage_univ_pi (π : ι ⊕ ι' → Type*) (t : ∀ i, Set (π i)) :
    (sumPiEquivProdPi π).symm ⁻¹' univ.pi t =
    univ.pi (fun i => t (.inl i)) ×ˢ univ.pi fun i => t (.inr i) := by
  ext
  simp_rw [mem_preimage, mem_prod, mem_univ_pi, sumPiEquivProdPi_symm_apply]
  constructor
  · intro h; constructor <;> intro i <;> apply h
  · rintro ⟨h₁, h₂⟩ (i|i) <;> simp <;> apply_assumption

Preimage of Universal Product Set under Sum-to-Product Equivalence Inverse

Informal description

For any family of types $\pi$ indexed by the sum type $\iota \oplus \iota'$ and any family of sets $t_i \subseteq \pi(i)$ for each $i \in \iota \oplus \iota'$, the preimage of the universal product set $\prod_{i \in \iota \oplus \iota'} t_i$ under the inverse of the equivalence $\text{sumPiEquivProdPi} \ \pi$ is equal to the Cartesian product of the universal product sets $\prod_{i \in \iota} t_{\text{inl}(i)}$ and $\prod_{i' \in \iota'} t_{\text{inr}(i')}$. In symbols: $$(\text{sumPiEquivProdPi} \ \pi)^{-1}\left(\prod_{i \in \iota \oplus \iota'} t_i\right) = \left(\prod_{i \in \iota} t_{\text{inl}(i)}\right) \times \left(\prod_{i' \in \iota'} t_{\text{inr}(i')}\right)$$

Set.mem_graphOn theorem

: x ∈ s.graphOn f ↔ x.1 ∈ s ∧ f x.1 = x.2

Full source

@[simp] lemma mem_graphOn : x ∈ s.graphOn fx ∈ s.graphOn f ↔ x.1 ∈ s ∧ f x.1 = x.2 := by aesop (add simp graphOn)

Characterization of Graph Membership: $(x, y) \in \text{graph}(f|_s) \leftrightarrow x \in s \land f(x) = y$

Informal description

For any function $f : \alpha \to \beta$ and set $s \subseteq \alpha$, a pair $(x, y)$ belongs to the graph of $f$ on $s$ if and only if $x \in s$ and $f(x) = y$.

Set.graphOn_empty theorem

(f : α → β) : graphOn f ∅ = ∅

Full source

@[simp] lemma graphOn_empty (f : α → β) : graphOn f ∅ = ∅ := image_empty _

Graph of Function on Empty Set is Empty

Informal description

For any function $f : \alpha \to \beta$, the graph of $f$ on the empty set is the empty set, i.e., $\{(x, f(x)) \mid x \in \emptyset\} = \emptyset$.

Set.graphOn_eq_empty theorem

: graphOn f s = ∅ ↔ s = ∅

Full source

@[simp] lemma graphOn_eq_empty : graphOngraphOn f s = ∅ ↔ s = ∅ := image_eq_empty

Empty Graph iff Empty Domain

Informal description

For any function $f : \alpha \to \beta$ and any set $s \subseteq \alpha$, the graph of $f$ on $s$ is empty if and only if $s$ is empty. In symbols: $$ \text{graph}(f, s) = \emptyset \leftrightarrow s = \emptyset $$

Set.graphOn_nonempty theorem

: (s.graphOn f).Nonempty ↔ s.Nonempty

Full source

@[simp] lemma graphOn_nonempty : (s.graphOn f).Nonempty ↔ s.Nonempty := image_nonempty

Nonempty Graph Equivalence: $\text{graph}(f, s) \neq \emptyset \iff s \neq \emptyset$

Informal description

For any function $f \colon \alpha \to \beta$ and any subset $s \subseteq \alpha$, the graph $\{(x, f(x)) \mid x \in s\}$ is nonempty if and only if $s$ is nonempty.

Set.graphOn_union theorem

(f : α → β) (s t : Set α) : graphOn f (s ∪ t) = graphOn f s ∪ graphOn f t

Full source

@[simp]
lemma graphOn_union (f : α → β) (s t : Set α) : graphOn f (s ∪ t) = graphOngraphOn f s ∪ graphOn f t :=
  image_union ..

Graph of Function Preserves Union

Informal description

For any function $f \colon \alpha \to \beta$ and any subsets $s, t \subseteq \alpha$, the graph of $f$ on the union $s \cup t$ is equal to the union of the graphs of $f$ on $s$ and $f$ on $t$. In symbols: $$ \mathrm{graph}(f, s \cup t) = \mathrm{graph}(f, s) \cup \mathrm{graph}(f, t) $$

Set.graphOn_singleton theorem

(f : α → β) (x : α) : graphOn f { x } = {(x, f x)}

Full source

@[simp]
lemma graphOn_singleton (f : α → β) (x : α) : graphOn f {x} = {(x, f x)} :=
  image_singleton ..

Graph of a Function on a Singleton Set is a Singleton Pair

Informal description

For any function $f : \alpha \to \beta$ and any element $x \in \alpha$, the graph of $f$ restricted to the singleton set $\{x\}$ is equal to the singleton set $\{(x, f(x))\}$.

Set.graphOn_insert theorem

(f : α → β) (x : α) (s : Set α) : graphOn f (insert x s) = insert (x, f x) (graphOn f s)

Full source

@[simp]
lemma graphOn_insert (f : α → β) (x : α) (s : Set α) :
    graphOn f (insert x s) = insert (x, f x) (graphOn f s) :=
  image_insert_eq ..

Graph of Function on Union with Singleton

Informal description

For any function $f \colon \alpha \to \beta$, element $x \in \alpha$, and subset $s \subseteq \alpha$, the graph of $f$ on the set $\{x\} \cup s$ is equal to the union of the singleton $\{(x, f(x))\}$ with the graph of $f$ on $s$. In other words, $$ \mathrm{graphOn}\, f\, (\{x\} \cup s) = \{(x, f(x))\} \cup \mathrm{graphOn}\, f\, s. $$

Set.image_fst_graphOn theorem

(f : α → β) (s : Set α) : Prod.fst '' graphOn f s = s

Full source

@[simp]
lemma image_fst_graphOn (f : α → β) (s : Set α) : Prod.fstProd.fst '' graphOn f s = s := by
  simp [graphOn, image_image]

First Projection of Graph Equals Domain

Informal description

For any function $f \colon \alpha \to \beta$ and any subset $s \subseteq \alpha$, the image of the graph of $f$ on $s$ under the first projection equals $s$ itself. In other words, $$ \mathrm{fst}''(\{(x, f(x)) \mid x \in s\}) = s. $$

Set.image_snd_graphOn theorem

(f : α → β) : Prod.snd '' s.graphOn f = f '' s

Full source

@[simp] lemma image_snd_graphOn (f : α → β) : Prod.sndProd.snd '' s.graphOn f = f '' s := by ext x; simp

Image of Graph's Second Projection Equals Function's Image

Informal description

For any function $f : \alpha \to \beta$ and set $s \subseteq \alpha$, the image of the graph of $f$ on $s$ under the second projection equals the image of $s$ under $f$. In other words, $\mathrm{snd}''(\{(x, f(x)) \mid x \in s\}) = \{f(x) \mid x \in s\}$.

Set.fst_injOn_graph theorem

: (s.graphOn f).InjOn Prod.fst

Full source

lemma fst_injOn_graph : (s.graphOn f).InjOn Prod.fst := by aesop (add simp InjOn)

Injectivity of First Projection on Graph of a Function

Informal description

For any function $f : \alpha \to \beta$ and any subset $s \subseteq \alpha$, the projection map $\mathrm{fst} : \alpha \times \beta \to \alpha$ is injective when restricted to the graph of $f$ on $s$, i.e., the set $\{(x, f(x)) \mid x \in s\}$.

Set.graphOn_comp theorem

(s : Set α) (f : α → β) (g : β → γ) : s.graphOn (g ∘ f) = (fun x ↦ (x.1, g x.2)) '' s.graphOn f

Full source

lemma graphOn_comp (s : Set α) (f : α → β) (g : β → γ) :
    s.graphOn (g ∘ f) = (fun x ↦ (x.1, g x.2)) '' s.graphOn f := by
  simpa using image_comp (fun x ↦ (x.1, g x.2)) (fun x ↦ (x, f x)) _

Graph of Function Composition Equals Transformed Graph

Informal description

For any set $s \subseteq \alpha$ and functions $f \colon \alpha \to \beta$ and $g \colon \beta \to \gamma$, the graph of the composition $g \circ f$ on $s$ is equal to the image of the graph of $f$ on $s$ under the map $(x, y) \mapsto (x, g(y))$. In symbols: $$\{(x, g(f(x))) \mid x \in s\} = \{(x, g(y)) \mid (x, y) \in \{(x, f(x)) \mid x \in s\}\}.$$

Set.graphOn_univ_eq_range theorem

: univ.graphOn f = range fun x ↦ (x, f x)

Full source

lemma graphOn_univ_eq_range : univ.graphOn f = range fun x ↦ (x, f x) := image_univ

Graph of Function on Universal Set Equals Range of Pairing Function

Informal description

The graph of a function $f : \alpha \to \beta$ on the universal set $\text{univ}$ is equal to the range of the function $x \mapsto (x, f(x))$. In other words, $\{(x, f(x)) \mid x \in \alpha\} = \{(x, y) \mid \exists x \in \alpha, y = f(x)\}$.

Set.graphOn_inj theorem

{g : α → β} : s.graphOn f = s.graphOn g ↔ s.EqOn f g

Full source

@[simp] lemma graphOn_inj {g : α → β} : s.graphOn f = s.graphOn g ↔ s.EqOn f g := by
  simp [Set.ext_iff, funext_iff, forall_swap, EqOn]

Graph Equality Implies Function Equality on a Set

Informal description

For any two functions $f, g : \alpha \to \beta$ and a set $s \subseteq \alpha$, the graphs of $f$ and $g$ on $s$ are equal if and only if $f$ and $g$ are equal on $s$. That is, the set $\{(x, f(x)) \mid x \in s\}$ equals $\{(x, g(x)) \mid x \in s\}$ if and only if $f(x) = g(x)$ for all $x \in s$.

Set.graphOn_prod_graphOn theorem

 (s : Set α) (t : Set β) (f : α → γ) (g : β → δ) :
  s.graphOn f ×ˢ t.graphOn g = Equiv.prodProdProdComm .. ⁻¹' (s ×ˢ t).graphOn (Prod.map f g)

Full source

lemma graphOn_prod_graphOn (s : Set α) (t : Set β) (f : α → γ) (g : β → δ) :
    s.graphOn f ×ˢ t.graphOn g = Equiv.prodProdProdCommEquiv.prodProdProdComm .. ⁻¹' (s ×ˢ t).graphOn (Prod.map f g) := by
  aesop

Product of Graphs Equals Rearranged Graph of Product Map

Informal description

For any sets $s \subseteq \alpha$, $t \subseteq \beta$ and functions $f : \alpha \to \gamma$, $g : \beta \to \delta$, the Cartesian product of the graphs of $f$ on $s$ and $g$ on $t$ is equal to the preimage under the rearrangement equivalence $\text{Equiv.prodProdProdComm}$ of the graph of the product map $\text{Prod.map } f g$ on $s \times t$. In symbols: $$ \text{graphOn}(f, s) \times \text{graphOn}(g, t) = (\text{Equiv.prodProdProdComm})^{-1}[\text{graphOn}(\text{Prod.map } f g, s \times t)] $$ where: - $\text{graphOn}(f, s) = \{(x, f(x)) \mid x \in s\}$ is the graph of $f$ restricted to $s$ - $\text{Prod.map } f g (x,y) = (f(x), g(y))$ is the product map - $\text{Equiv.prodProdProdComm}$ is the bijection that rearranges $((a,b),(c,d)) \mapsto ((a,c),(b,d))$

Set.graphOn_prod_prodMap theorem

 (s : Set α) (t : Set β) (f : α → γ) (g : β → δ) :
  (s ×ˢ t).graphOn (Prod.map f g) = Equiv.prodProdProdComm .. ⁻¹' s.graphOn f ×ˢ t.graphOn g

Full source

lemma graphOn_prod_prodMap (s : Set α) (t : Set β) (f : α → γ) (g : β → δ) :
    (s ×ˢ t).graphOn (Prod.map f g) = Equiv.prodProdProdCommEquiv.prodProdProdComm .. ⁻¹' s.graphOn f ×ˢ t.graphOn g := by
  aesop

Graph of Product Map on Product Set Equals Rearranged Product of Graphs

Informal description

For any sets $s \subseteq \alpha$ and $t \subseteq \beta$, and functions $f : \alpha \to \gamma$ and $g : \beta \to \delta$, the graph of the product map $\mathrm{Prod.map}\, f\, g$ on the product set $s \timesˢ t$ is equal to the preimage under the equivalence $\mathrm{Equiv.prodProdProdComm}$ of the product of the graphs of $f$ on $s$ and $g$ on $t$. In other words, the following equality holds: $$ \mathrm{graphOn}\, (s \timesˢ t)\, (\mathrm{Prod.map}\, f\, g) = \mathrm{Equiv.prodProdProdComm}^{-1}(\mathrm{graphOn}\, s\, f \timesˢ \mathrm{graphOn}\, t\, g) $$ where $\mathrm{graphOn}\, X\, h$ denotes the graph $\{(x, h(x)) \mid x \in X\}$ of the function $h$ on the set $X$.

Set.exists_range_eq_graphOn_univ theorem

 {f : α → β × γ} (hf₁ : Surjective (Prod.fst ∘ f)) (hf : ∀ g₁ g₂, (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2) :
  ∃ f' : β → γ, range f = univ.graphOn f'

Full source

/-- **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' : β → γ`. -/
lemma exists_range_eq_graphOn_univ {f : α → β × γ} (hf₁ : Surjective (Prod.fstProd.fst ∘ f))
    (hf : ∀ g₁ g₂, (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2) :
    ∃ f' : β → γ, range f = univ.graphOn f' := by
  refine ⟨fun h ↦ (f (hf₁ h).choose).snd, ?_⟩
  ext x
  simp only [mem_range, comp_apply, mem_graphOn, mem_univ, true_and]
  refine ⟨?_, fun hi ↦ ⟨(hf₁ x.1).choose, Prod.ext (hf₁ x.1).choose_spec hi⟩⟩
  rintro ⟨g, rfl⟩
  exact hf _ _ (hf₁ (f g).1).choose_spec

Vertical Line Test for Function Graphs

Informal description

Let $f : \alpha \to \beta \times \gamma$ be a function to a product type. Suppose that: 1. The composition $\pi_1 \circ f$ is surjective (where $\pi_1$ is the first projection), and 2. For any $g_1, g_2 \in \alpha$, if the first components of $f(g_1)$ and $f(g_2)$ are equal, then their second components must also be equal. Then there exists a function $f' : \beta \to \gamma$ such that the range of $f$ equals the graph of $f'$ on the universal set, i.e., $\text{range}(f) = \{(b, f'(b)) \mid b \in \beta\}$.

Set.exists_equiv_range_eq_graphOn_univ theorem

 {f : α → β × γ} (hf₁ : Surjective (Prod.fst ∘ f)) (hf₂ : Surjective (Prod.snd ∘ f))
  (hf : ∀ g₁ g₂, (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2) : ∃ e : β ≃ γ, range f = univ.graphOn e

Full source

/-- **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' : β ≃ γ`. -/
lemma exists_equiv_range_eq_graphOn_univ {f : α → β × γ} (hf₁ : Surjective (Prod.fstProd.fst ∘ f))
    (hf₂ : Surjective (Prod.sndProd.snd ∘ f)) (hf : ∀ g₁ g₂, (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2) :
    ∃ e : β ≃ γ, range f = univ.graphOn e := by
  obtain ⟨e₁, he₁⟩ := exists_range_eq_graphOn_univ hf₁ fun _ _ ↦ (hf _ _).1
  obtain ⟨e₂, he₂⟩ := exists_range_eq_graphOn_univ (f := Equiv.prodCommEquiv.prodComm _ _ ∘ f) (by simpa) <|
    by simp [hf]
  have he₁₂ h i : e₁ h = i ↔ e₂ i = h := by
    rw [Set.ext_iff] at he₁ he₂
    aesop (add simp [Prod.swap_eq_iff_eq_swap])
  exact ⟨
  { toFun := e₁
    invFun := e₂
    left_inv := fun h ↦ by rw [← he₁₂]
    right_inv := fun i ↦ by rw [he₁₂] }, he₁⟩

Graph Characterization of Equivalences via Vertical and Horizontal Line Tests

Informal description

Let $f : \alpha \to \beta \times \gamma$ be a function to a product type. Suppose that: 1. The composition $\pi_1 \circ f$ is surjective (where $\pi_1$ is the first projection), 2. The composition $\pi_2 \circ f$ is surjective (where $\pi_2$ is the second projection), and 3. For any $g_1, g_2 \in \alpha$, the first components of $f(g_1)$ and $f(g_2)$ are equal if and only if their second components are equal. Then there exists an equivalence (bijection) $e : \beta \simeq \gamma$ such that the range of $f$ equals the graph of $e$ on the universal set, i.e., $\text{range}(f) = \{(b, e(b)) \mid b \in \beta\}$.

Set.exists_eq_mgraphOn_univ theorem

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

Full source

/-- **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 : β → γ`. -/
lemma exists_eq_mgraphOn_univ {s : Set (β × γ)}
    (hs₁ : Bijective (Prod.fstProd.fst ∘ (Subtype.val : s → β × γ))) : ∃ f : β → γ, s = univ.graphOn f := by
  simpa using exists_range_eq_graphOn_univ hs₁.surjective
    fun a b h ↦ congr_arg (Prod.sndProd.snd ∘ (Subtype.val : s → β × γ)) (hs₁.injective h)

Vertical Line Test for Graphs of Functions

Informal description

Let $s \subseteq \beta \times \gamma$ be a subset of the product type. If the restriction of the first projection $\pi_1$ to $s$ is bijective, then there exists a function $f : \beta \to \gamma$ such that $s$ is equal to the graph of $f$ on the universal set, i.e., $s = \{(b, f(b)) \mid b \in \beta\}$.

Main declarations