Mathlib.Data.Finset.Prod

Finset.product definition

(s : Finset α) (t : Finset β) : Finset (α × β)

Full source

/-- `product s t` is the set of pairs `(a, b)` such that `a ∈ s` and `b ∈ t`. -/
protected def product (s : Finset α) (t : Finset β) : Finset (α × β) :=
  ⟨_, s.nodup.product t.nodup⟩

Cartesian product of finite sets

Informal description

For finite sets $s \subseteq \alpha$ and $t \subseteq \beta$, the product $s \times t$ is the finite set of all pairs $(a, b)$ where $a \in s$ and $b \in t$.

Finset.instSProd instance

: SProd (Finset α) (Finset β) (Finset (α × β))

Full source

instance instSProd : SProd (Finset α) (Finset β) (Finset (α × β)) where
  sprod := Finset.product

Cartesian Product Operation for Finite Sets

Informal description

For any types $\alpha$ and $\beta$, the finite sets of $\alpha$ and $\beta$ can be multiplied using the operation $\timesˢ$ to form a finite set of pairs in $\alpha \times \beta$. This operation coincides with the Cartesian product of finite sets.

Finset.product_eq_sprod theorem

: Finset.product s t = s ×ˢ t

Full source

@[simp]
theorem product_eq_sprod : Finset.product s t = s ×ˢ t :=
  rfl

Equality of Cartesian Product and Finite Set Product: $s \times t = s \timesˢ t$

Informal description

For any finite sets $s \subseteq \alpha$ and $t \subseteq \beta$, the Cartesian product $s \times t$ is equal to the finite set product $s \timesˢ t$.

Finset.product_val theorem

: (s ×ˢ t).1 = s.1 ×ˢ t.1

Full source

@[simp]
theorem product_val : (s ×ˢ t).1 = s.1 ×ˢ t.1 :=
  rfl

Underlying Multiset of Cartesian Product of Finite Sets

Informal description

For any finite sets $s$ of type $\alpha$ and $t$ of type $\beta$, the underlying multiset of their Cartesian product $s \timesˢ t$ is equal to the Cartesian product of the underlying multisets of $s$ and $t$. In other words, $(s \timesˢ t).1 = s.1 \timesˢ t.1$.

Finset.mem_product theorem

{p : α × β} : p ∈ s ×ˢ t ↔ p.1 ∈ s ∧ p.2 ∈ t

Full source

@[simp]
theorem mem_product {p : α × β} : p ∈ s ×ˢ tp ∈ s ×ˢ t ↔ p.1 ∈ s ∧ p.2 ∈ t :=
  Multiset.mem_product

Membership in Cartesian Product of Finite Sets: $(a, b) \in s \times t \leftrightarrow a \in s \land b \in t$

Informal description

For any pair $p = (a, b)$ in $\alpha \times \beta$, $p$ belongs to the Cartesian product $s \timesˢ t$ of finite sets $s \subseteq \alpha$ and $t \subseteq \beta$ if and only if $a \in s$ and $b \in t$.

Finset.mk_mem_product theorem

(ha : a ∈ s) (hb : b ∈ t) : (a, b) ∈ s ×ˢ t

Full source

theorem mk_mem_product (ha : a ∈ s) (hb : b ∈ t) : (a, b)(a, b) ∈ s ×ˢ t :=
  mem_product.2 ⟨ha, hb⟩

Membership of Pair in Cartesian Product of Finite Sets

Informal description

For any elements $a \in s$ and $b \in t$ where $s$ is a finite subset of $\alpha$ and $t$ is a finite subset of $\beta$, the pair $(a, b)$ belongs to the Cartesian product $s \times t$ of the finite sets.

Finset.coe_product theorem

(s : Finset α) (t : Finset β) : (↑(s ×ˢ t) : Set (α × β)) = (s : Set α) ×ˢ t

Full source

@[simp, norm_cast]
theorem coe_product (s : Finset α) (t : Finset β) :
    (↑(s ×ˢ t) : Set (α × β)) = (s : Set α) ×ˢ t :=
  Set.ext fun _ => Finset.mem_product

Equality of Finite and Set Cartesian Products: $(s \timesˢ t) = s \times t$

Informal description

For any finite sets $s \subseteq \alpha$ and $t \subseteq \beta$, the underlying set of their Cartesian product $s \timesˢ t$ is equal to the Cartesian product of their underlying sets, i.e., $(s \timesˢ t) = s \times t$ as sets.

Finset.subset_product_image_fst theorem

[DecidableEq α] : (s ×ˢ t).image Prod.fst ⊆ s

Full source

theorem subset_product_image_fst [DecidableEq α] : (s ×ˢ t).image Prod.fst ⊆ s := fun i => by
  simp +contextual [mem_image]

First Projection of Cartesian Product is Subset of First Factor

Informal description

For any finite sets $s \subseteq \alpha$ and $t \subseteq \beta$, the image of the Cartesian product $s \times t$ under the first projection $\pi_1$ is a subset of $s$, i.e., $\pi_1(s \times t) \subseteq s$.

Finset.subset_product_image_snd theorem

[DecidableEq β] : (s ×ˢ t).image Prod.snd ⊆ t

Full source

theorem subset_product_image_snd [DecidableEq β] : (s ×ˢ t).image Prod.snd ⊆ t := fun i => by
  simp +contextual [mem_image]

Projection of Cartesian Product onto Second Factor is Subset

Informal description

For any finite sets $s \subseteq \alpha$ and $t \subseteq \beta$, the image of the Cartesian product $s \times t$ under the second projection $\mathrm{snd} : \alpha \times \beta \to \beta$ is a subset of $t$.

Finset.product_image_fst theorem

[DecidableEq α] (ht : t.Nonempty) : (s ×ˢ t).image Prod.fst = s

Full source

theorem product_image_fst [DecidableEq α] (ht : t.Nonempty) : (s ×ˢ t).image Prod.fst = s := by
  ext i
  simp [mem_image, ht.exists_mem]

First Projection Image of Nonempty Cartesian Product Equals First Factor

Informal description

For any finite sets $s$ of type $\alpha$ and $t$ of type $\beta$, if $t$ is nonempty, then the image of the first projection on the Cartesian product $s \times t$ equals $s$. That is, $\text{image}(\pi_1, s \times t) = s$, where $\pi_1$ denotes the first projection map $(a, b) \mapsto a$.

Finset.product_image_snd theorem

[DecidableEq β] (ht : s.Nonempty) : (s ×ˢ t).image Prod.snd = t

Full source

theorem product_image_snd [DecidableEq β] (ht : s.Nonempty) : (s ×ˢ t).image Prod.snd = t := by
  ext i
  simp [mem_image, ht.exists_mem]

Image of Cartesian Product under Second Projection Equals Second Factor for Nonempty Finite Sets

Informal description

For any nonempty finite set $s$ of elements of type $\alpha$ and any finite set $t$ of elements of type $\beta$, the image of the Cartesian product $s \times t$ under the second projection $\mathrm{snd} : \alpha \times \beta \to \beta$ is equal to $t$.

Finset.subset_product theorem

[DecidableEq α] [DecidableEq β] {s : Finset (α × β)} : s ⊆ s.image Prod.fst ×ˢ s.image Prod.snd

Full source

theorem subset_product [DecidableEq α] [DecidableEq β] {s : Finset (α × β)} :
    s ⊆ s.image Prod.fst ×ˢ s.image Prod.snd := fun _ hp =>
  mem_product.2 ⟨mem_image_of_mem _ hp, mem_image_of_mem _ hp⟩

Finite Set is Subset of Product of its Projections

Informal description

For any finite set $s$ of pairs in $\alpha \times \beta$, the set $s$ is a subset of the Cartesian product of the image of $s$ under the first projection and the image of $s$ under the second projection. That is, $s \subseteq \pi_1(s) \times \pi_2(s)$, where $\pi_1$ and $\pi_2$ denote the first and second projection maps respectively.

Finset.product_subset_product theorem

(hs : s ⊆ s') (ht : t ⊆ t') : s ×ˢ t ⊆ s' ×ˢ t'

Full source

@[gcongr]
theorem product_subset_product (hs : s ⊆ s') (ht : t ⊆ t') : s ×ˢ t ⊆ s' ×ˢ t' := fun ⟨_, _⟩ h =>
  mem_product.2 ⟨hs (mem_product.1 h).1, ht (mem_product.1 h).2⟩

Cartesian Product Preserves Subset Relation

Informal description

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

Finset.product_subset_product_left theorem

(hs : s ⊆ s') : s ×ˢ t ⊆ s' ×ˢ t

Full source

@[gcongr]
theorem product_subset_product_left (hs : s ⊆ s') : s ×ˢ t ⊆ s' ×ˢ t :=
  product_subset_product hs (Subset.refl _)

Left Factor Subset Implies Cartesian Product Subset

Informal description

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

Finset.product_subset_product_right theorem

(ht : t ⊆ t') : s ×ˢ t ⊆ s ×ˢ t'

Full source

@[gcongr]
theorem product_subset_product_right (ht : t ⊆ t') : s ×ˢ t ⊆ s ×ˢ t' :=
  product_subset_product (Subset.refl _) ht

Right Factor Subset Implies Cartesian Product Subset

Informal description

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

Finset.prodMap_image_product theorem

 {δ : Type*} [DecidableEq β] [DecidableEq δ] (f : α → β) (g : γ → δ) (s : Finset α) (t : Finset γ) :
  (s ×ˢ t).image (Prod.map f g) = s.image f ×ˢ t.image g

Full source

theorem prodMap_image_product {δ : Type*} [DecidableEq β] [DecidableEq δ]
    (f : α → β) (g : γ → δ) (s : Finset α) (t : Finset γ) :
    (s ×ˢ t).image (Prod.map f g) = s.image f ×ˢ t.image g :=
  mod_cast Set.prodMap_image_prod f g s t

Image of Cartesian Product under Product Map Equals Product of Images for Finite Sets

Informal description

For any finite 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)$$

Finset.prodMap_map_product theorem

 {δ : Type*} (f : α ↪ β) (g : γ ↪ δ) (s : Finset α) (t : Finset γ) : (s ×ˢ t).map (f.prodMap g) = s.map f ×ˢ t.map g

Full source

theorem prodMap_map_product {δ : Type*} (f : α ↪ β) (g : γ ↪ δ) (s : Finset α) (t : Finset γ) :
    (s ×ˢ t).map (f.prodMap g) = s.map f ×ˢ t.map g := by
  simpa [← coe_inj] using Set.prodMap_image_prod f g s t

Image of Finite Cartesian Product under Product of Injective Maps Equals Product of Images

Informal description

For any finite sets $s \subseteq \alpha$ and $t \subseteq \gamma$, and any injective functions $f : \alpha \hookrightarrow \beta$ and $g : \gamma \hookrightarrow \delta$, the image of the Cartesian product $s \times t$ under the product map $(f \times 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)$$

Finset.map_swap_product theorem

(s : Finset α) (t : Finset β) : (t ×ˢ s).map ⟨Prod.swap, Prod.swap_injective⟩ = s ×ˢ t

Full source

theorem map_swap_product (s : Finset α) (t : Finset β) :
    (t ×ˢ s).map ⟨Prod.swap, Prod.swap_injective⟩ = s ×ˢ t :=
  coe_injective <| by
    push_cast
    exact Set.image_swap_prod _ _

Image of Finite Cartesian Product under Swap Equals Swapped Product

Informal description

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

Finset.image_swap_product theorem

[DecidableEq (α × β)] (s : Finset α) (t : Finset β) : (t ×ˢ s).image Prod.swap = s ×ˢ t

Full source

@[simp]
theorem image_swap_product [DecidableEq (α × β)] (s : Finset α) (t : Finset β) :
    (t ×ˢ s).image Prod.swap = s ×ˢ t :=
  coe_injective <| by
    push_cast
    exact Set.image_swap_prod _ _

Image of Finite Cartesian Product under Swap Equals Swapped Product

Informal description

For any finite sets $s \subseteq \alpha$ and $t \subseteq \beta$, the image of the Cartesian product $t \times s$ under the swap function $\mathrm{swap} : \beta \times \alpha \to \alpha \times \beta$ is equal to the Cartesian product $s \times t$. That is, $$\mathrm{swap}(t \times s) = s \times t$$ where $\mathrm{swap}(b,a) = (a,b)$ swaps the components of each pair.

Finset.product_eq_biUnion theorem

[DecidableEq (α × β)] (s : Finset α) (t : Finset β) : s ×ˢ t = s.biUnion fun a => t.image fun b => (a, b)

Full source

theorem product_eq_biUnion [DecidableEq (α × β)] (s : Finset α) (t : Finset β) :
    s ×ˢ t = s.biUnion fun a => t.image fun b => (a, b) :=
  ext fun ⟨x, y⟩ => by
    simp only [mem_product, mem_biUnion, mem_image, exists_prop, Prod.mk_inj, and_left_comm,
      exists_and_left, exists_eq_right, exists_eq_left]

Cartesian Product as Union of Images

Informal description

For finite sets $s \subseteq \alpha$ and $t \subseteq \beta$, the Cartesian product $s \times t$ is equal to the finite union over $a \in s$ of the images of the functions $\lambda b, (a, b)$ applied to $t$. That is, $$ s \times t = \bigcup_{a \in s} \{(a, b) \mid b \in t\}. $$

Finset.product_eq_biUnion_right theorem

[DecidableEq (α × β)] (s : Finset α) (t : Finset β) : s ×ˢ t = t.biUnion fun b => s.image fun a => (a, b)

Full source

theorem product_eq_biUnion_right [DecidableEq (α × β)] (s : Finset α) (t : Finset β) :
    s ×ˢ t = t.biUnion fun b => s.image fun a => (a, b) :=
  ext fun ⟨x, y⟩ => by
    simp only [mem_product, mem_biUnion, mem_image, exists_prop, Prod.mk_inj, and_left_comm,
      exists_and_left, exists_eq_right, exists_eq_left]

Cartesian Product as Right-indexed Union of Images

Informal description

For any finite sets $s \subseteq \alpha$ and $t \subseteq \beta$, the Cartesian product $s \times t$ is equal to the finite union over $b \in t$ of the images of the functions $\lambda a, (a, b)$ applied to $s$. That is, $$ s \times t = \bigcup_{b \in t} \{(a, b) \mid a \in s\}. $$

Finset.product_biUnion theorem

 [DecidableEq γ] (s : Finset α) (t : Finset β) (f : α × β → Finset γ) :
  (s ×ˢ t).biUnion f = s.biUnion fun a => t.biUnion fun b => f (a, b)

Full source

/-- See also `Finset.sup_product_left`. -/
@[simp]
theorem product_biUnion [DecidableEq γ] (s : Finset α) (t : Finset β) (f : α × β → Finset γ) :
    (s ×ˢ t).biUnion f = s.biUnion fun a => t.biUnion fun b => f (a, b) := by
  classical simp_rw [product_eq_biUnion, biUnion_biUnion, image_biUnion]

Double Union Equals Union Over Product for Finite Sets: $\bigcup_{(a,b) \in s \times t} f(a,b) = \bigcup_{a \in s} \bigcup_{b \in t} f(a,b)$

Informal description

Let $s \subseteq \alpha$ and $t \subseteq \beta$ be finite sets, and let $f : \alpha \times \beta \to \text{Finset} \gamma$ be a function. Then the finite union of $f$ over the Cartesian product $s \times t$ is equal to the double finite union of $f$ over $s$ and $t$: \[ \bigcup_{(a,b) \in s \times t} f(a,b) = \bigcup_{a \in s} \bigcup_{b \in t} f(a,b). \]

Finset.card_product theorem

(s : Finset α) (t : Finset β) : card (s ×ˢ t) = card s * card t

Full source

@[simp]
theorem card_product (s : Finset α) (t : Finset β) : card (s ×ˢ t) = card s * card t :=
  Multiset.card_product _ _

Cardinality of Cartesian Product of Finite Sets: $|s \times t| = |s| \cdot |t|$

Informal description

For any finite sets $s \subseteq \alpha$ and $t \subseteq \beta$, the cardinality of their Cartesian product $s \times t$ is equal to the product of the cardinalities of $s$ and $t$. That is, \[ |s \times t| = |s| \cdot |t|. \]

Finset.nontrivial_prod_iff theorem

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

Full source

/-- The product of two Finsets is nontrivial iff both are nonempty
  at least one of them is nontrivial. -/
lemma nontrivial_prod_iff : (s ×ˢ t).Nontrivial ↔
    s.Nonempty ∧ t.Nonempty ∧ (s.Nontrivial ∨ t.Nontrivial) := by
  simp_rw [← card_pos, ← one_lt_card_iff_nontrivial, card_product]; apply Nat.one_lt_mul_iff

Nontriviality Criterion for Cartesian Product of Finite Sets: $s \times t$ is nontrivial iff $s$ and $t$ are nonempty and at least one is nontrivial

Informal description

For any finite sets $s \subseteq \alpha$ and $t \subseteq \beta$, the Cartesian product $s \times t$ is nontrivial (contains at least two distinct elements) if and only if both $s$ and $t$ are nonempty, and at least one of them is nontrivial (contains at least two distinct elements). In other words: \[ s \times t \text{ is nontrivial} \iff s \neq \emptyset \land t \neq \emptyset \land (s \text{ is nontrivial} \lor t \text{ is nontrivial}). \]

Finset.filter_product theorem

 (p : α → Prop) (q : β → Prop) [DecidablePred p] [DecidablePred q] :
  ((s ×ˢ t).filter fun x : α × β => p x.1 ∧ q x.2) = s.filter p ×ˢ t.filter q

Full source

theorem filter_product (p : α → Prop) (q : β → Prop) [DecidablePred p] [DecidablePred q] :
    ((s ×ˢ t).filter fun x : α × β => p x.1 ∧ q x.2) = s.filter p ×ˢ t.filter q := by
  ext ⟨a, b⟩
  simp [mem_filter, mem_product, decide_eq_true_eq, and_comm, and_left_comm, and_assoc]

Filtered Product Set Equality: $\{(x,y) \in s \times t \mid p(x) \land q(y)\} = \{x \in s \mid p(x)\} \times \{y \in t \mid q(y)\}$

Informal description

Let $s$ be a finite subset of a type $\alpha$ and $t$ a finite subset of a type $\beta$. For any decidable predicates $p : \alpha \to \text{Prop}$ and $q : \beta \to \text{Prop}$, the filtered product set $\{(x,y) \in s \times t \mid p(x) \land q(y)\}$ is equal to the product of the filtered sets $\{x \in s \mid p(x)\} \times \{y \in t \mid q(y)\}$.

Finset.filter_product_left theorem

(p : α → Prop) [DecidablePred p] : ((s ×ˢ t).filter fun x : α × β => p x.1) = s.filter p ×ˢ t

Full source

theorem filter_product_left (p : α → Prop) [DecidablePred p] :
    ((s ×ˢ t).filter fun x : α × β => p x.1) = s.filter p ×ˢ t := by
  simpa using filter_product p fun _ => true

Filtered Product Set Equality (Left Factor): $\{(x,y) \in s \times t \mid p(x)\} = \{x \in s \mid p(x)\} \times t$

Informal description

Let $s$ be a finite subset of a type $\alpha$ and $t$ a finite subset of a type $\beta$. For any decidable predicate $p : \alpha \to \text{Prop}$, the filtered product set $\{(x,y) \in s \times t \mid p(x)\}$ is equal to the product of the filtered set $\{x \in s \mid p(x)\}$ with $t$, i.e., \[ \{(x,y) \in s \times t \mid p(x)\} = \{x \in s \mid p(x)\} \times t. \]

Finset.filter_product_right theorem

(q : β → Prop) [DecidablePred q] : ((s ×ˢ t).filter fun x : α × β => q x.2) = s ×ˢ t.filter q

Full source

theorem filter_product_right (q : β → Prop) [DecidablePred q] :
    ((s ×ˢ t).filter fun x : α × β => q x.2) = s ×ˢ t.filter q := by
  simpa using filter_product (fun _ : α => true) q

Right-Filtered Product Set Equality: $\{(x,y) \in s \times t \mid q(y)\} = s \times \{y \in t \mid q(y)\}$

Informal description

Let $s$ be a finite subset of a type $\alpha$ and $t$ a finite subset of a type $\beta$. For any decidable predicate $q : \beta \to \text{Prop}$, the filtered product set $\{(x,y) \in s \times t \mid q(y)\}$ is equal to the product $s \times \{y \in t \mid q(y)\}$.

Finset.filter_product_card theorem

 (s : Finset α) (t : Finset β) (p : α → Prop) (q : β → Prop) [DecidablePred p] [DecidablePred q] :
  ((s ×ˢ t).filter fun x : α × β => (p x.1) = (q x.2)).card =
    (s.filter p).card * (t.filter q).card + (s.filter (¬p ·)).card * (t.filter (¬q ·)).card

Full source

theorem filter_product_card (s : Finset α) (t : Finset β) (p : α → Prop) (q : β → Prop)
    [DecidablePred p] [DecidablePred q] :
    ((s ×ˢ t).filter fun x : α × β => (p x.1) = (q x.2)).card =
      (s.filter p).card * (t.filter q).card +
        (s.filter (¬ p ·)).card * (t.filter (¬ q ·)).card := by
  classical
  rw [← card_product, ← card_product, ← filter_product, ← filter_product, ← card_union_of_disjoint]
  · apply congr_arg
    ext ⟨a, b⟩
    simp only [filter_union_right, mem_filter, mem_product]
    constructor <;> intro h <;> use h.1
    · simp only [h.2, Function.comp_apply, Decidable.em, and_self]
    · revert h
      simp only [Function.comp_apply, and_imp]
      rintro _ _ (_|_) <;> simp [*]
  · apply Finset.disjoint_filter_filter'
    exact (disjoint_compl_right.inf_left _).inf_right _

Cardinality of Filtered Product Set by Predicate Equality: $|\{(x,y) \in s \times t \mid p(x) = q(y)\}| = |s_p| \cdot |t_q| + |s_{\neg p}| \cdot |t_{\neg q}|$

Informal description

For any finite sets $s \subseteq \alpha$ and $t \subseteq \beta$, and any decidable predicates $p : \alpha \to \text{Prop}$ and $q : \beta \to \text{Prop}$, the cardinality of the filtered product set $\{(x,y) \in s \times t \mid p(x) = q(y)\}$ is equal to: \[ |\{x \in s \mid p(x)\}| \cdot |\{y \in t \mid q(y)\}| + |\{x \in s \mid \neg p(x)\}| \cdot |\{y \in t \mid \neg q(y)\}|. \]

Finset.empty_product theorem

(t : Finset β) : (∅ : Finset α) ×ˢ t = ∅

Full source

@[simp]
theorem empty_product (t : Finset β) : (∅ : Finset α) ×ˢ t = ∅ :=
  rfl

Empty Set Left Annihilator for Cartesian Product of Finite Sets

Informal description

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

Finset.product_empty theorem

(s : Finset α) : s ×ˢ (∅ : Finset β) = ∅

Full source

@[simp]
theorem product_empty (s : Finset α) : s ×ˢ (∅ : Finset β) = ∅ :=
  eq_empty_of_forall_not_mem fun _ h => not_mem_empty _ (Finset.mem_product.1 h).2

Right Annihilator of Cartesian Product with Empty Set

Informal description

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

Finset.Nonempty.product theorem

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

Full source

@[aesop safe apply (rule_sets := [finsetNonempty])]
theorem Nonempty.product (hs : s.Nonempty) (ht : t.Nonempty) : (s ×ˢ t).Nonempty :=
  let ⟨x, hx⟩ := hs
  let ⟨y, hy⟩ := ht
  ⟨(x, y), mem_product.2 ⟨hx, hy⟩⟩

Nonempty Cartesian Product of Nonempty Finite Sets

Informal description

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

Finset.Nonempty.fst theorem

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

Full source

theorem Nonempty.fst (h : (s ×ˢ t).Nonempty) : s.Nonempty :=
  let ⟨xy, hxy⟩ := h
  ⟨xy.1, (mem_product.1 hxy).1⟩

Nonemptiness of First Component in Nonempty Cartesian Product

Informal description

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

Finset.Nonempty.snd theorem

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

Full source

theorem Nonempty.snd (h : (s ×ˢ t).Nonempty) : t.Nonempty :=
  let ⟨xy, hxy⟩ := h
  ⟨xy.2, (mem_product.1 hxy).2⟩

Nonemptiness of Second Factor in Nonempty Cartesian Product

Informal description

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

Finset.nonempty_product theorem

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

Full source

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

Nonemptiness of Cartesian Product of Finite Sets

Informal description

For any finite sets $s \subseteq \alpha$ and $t \subseteq \beta$, the Cartesian product $s \times t$ is nonempty if and only if both $s$ and $t$ are nonempty. In symbols: $$ s \times t \neq \emptyset \iff s \neq \emptyset \text{ and } t \neq \emptyset. $$

Finset.product_eq_empty theorem

{s : Finset α} {t : Finset β} : s ×ˢ t = ∅ ↔ s = ∅ ∨ t = ∅

Full source

@[simp]
theorem product_eq_empty {s : Finset α} {t : Finset β} : s ×ˢ t = ∅ ↔ s = ∅ ∨ t = ∅ := by
  rw [← not_nonempty_iff_eq_empty, nonempty_product, not_and_or, not_nonempty_iff_eq_empty,
    not_nonempty_iff_eq_empty]

Empty Cartesian Product Characterization: $s \times t = \emptyset \iff s = \emptyset \lor t = \emptyset$

Informal description

For any finite sets $s \subseteq \alpha$ and $t \subseteq \beta$, the Cartesian product $s \times t$ is empty if and only if either $s$ is empty or $t$ is empty. In symbols: $$ s \times t = \emptyset \iff s = \emptyset \text{ or } t = \emptyset. $$

Finset.singleton_product theorem

{a : α} : ({ a } : Finset α) ×ˢ t = t.map ⟨Prod.mk a, Prod.mk_right_injective _⟩

Full source

@[simp]
theorem singleton_product {a : α} :
    ({a} : Finset α) ×ˢ t = t.map ⟨Prod.mk a, Prod.mk_right_injective _⟩ := by
  ext ⟨x, y⟩
  simp [and_left_comm, eq_comm]

Cartesian Product of Singleton with Finite Set Equals Image of Pairing Function

Informal description

For any element $a$ of type $\alpha$ and any finite set $t$ of type $\beta$, the Cartesian product of the singleton set $\{a\}$ with $t$ is equal to the image of $t$ under the injective function that maps each element $b \in \beta$ to the pair $(a, b)$. In symbols: $$ \{a\} \times t = \{(a, b) \mid b \in t\}. $$

Finset.product_singleton theorem

: s ×ˢ { b } = s.map ⟨fun i => (i, b), Prod.mk_left_injective _⟩

Full source

@[simp]
lemma product_singleton : s ×ˢ {b} = s.map ⟨fun i => (i, b), Prod.mk_left_injective _⟩ := by
  ext ⟨x, y⟩
  simp [and_left_comm, eq_comm]

Cartesian Product with Singleton: $s \times \{b\} = \text{map}(i \mapsto (i, b), s)$

Informal description

For any finite set $s$ of type $\alpha$ and any element $b \in \beta$, the Cartesian product $s \times \{b\}$ is equal to the image of $s$ under the injective map $i \mapsto (i, b)$.

Finset.singleton_product_singleton theorem

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

Full source

theorem singleton_product_singleton {a : α} {b : β} :
    ({a} ×ˢ {b} : Finset _) = {(a, b)} := by
  simp only [product_singleton, Function.Embedding.coeFn_mk, map_singleton]

Cartesian Product of Singletons: $\{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$.

Finset.union_product theorem

[DecidableEq α] [DecidableEq β] : (s ∪ s') ×ˢ t = s ×ˢ t ∪ s' ×ˢ t

Full source

@[simp]
theorem union_product [DecidableEq α] [DecidableEq β] : (s ∪ s') ×ˢ t = s ×ˢ t ∪ s' ×ˢ t := by
  ext ⟨x, y⟩
  simp only [or_and_right, mem_union, mem_product]

Distributivity of Cartesian Product over Union of Finite Sets

Informal description

For any finite sets $s, s'$ of type $\alpha$ and $t$ of type $\beta$, the Cartesian product of the union $s \cup s'$ with $t$ is equal to the union of the Cartesian products $s \times t$ and $s' \times t$, i.e., $(s \cup s') \times t = (s \times t) \cup (s' \times t)$.

Finset.product_union theorem

[DecidableEq α] [DecidableEq β] : s ×ˢ (t ∪ t') = s ×ˢ t ∪ s ×ˢ t'

Full source

@[simp]
theorem product_union [DecidableEq α] [DecidableEq β] : s ×ˢ (t ∪ t') = s ×ˢ t ∪ s ×ˢ t' := by
  ext ⟨x, y⟩
  simp only [and_or_left, mem_union, mem_product]

Distributivity of Cartesian Product over Union of Finite Sets

Informal description

For any finite sets $s$ of type $\alpha$ and $t, t'$ of type $\beta$, the Cartesian product $s \times (t \cup t')$ is equal to $(s \times t) \cup (s \times t')$.

Finset.inter_product theorem

[DecidableEq α] [DecidableEq β] : (s ∩ s') ×ˢ t = s ×ˢ t ∩ s' ×ˢ t

Full source

theorem inter_product [DecidableEq α] [DecidableEq β] : (s ∩ s') ×ˢ t = s ×ˢ t ∩ s' ×ˢ t := by
  ext ⟨x, y⟩
  simp only [← and_and_right, mem_inter, mem_product]

Cartesian Product Distributes Over Intersection: $(s \cap s') \times t = (s \times t) \cap (s' \times t)$

Informal description

For any finite sets $s, s'$ of type $\alpha$ and $t$ of type $\beta$ (with decidable equality on both types), the Cartesian product of the intersection $s \cap s'$ with $t$ equals the intersection of the Cartesian products $s \times t$ and $s' \times t$. In symbols: $$(s \cap s') \times t = (s \times t) \cap (s' \times t)$$

Finset.product_inter theorem

[DecidableEq α] [DecidableEq β] : s ×ˢ (t ∩ t') = s ×ˢ t ∩ s ×ˢ t'

Full source

theorem product_inter [DecidableEq α] [DecidableEq β] : s ×ˢ (t ∩ t') = s ×ˢ t ∩ s ×ˢ t' := by
  ext ⟨x, y⟩
  simp only [← and_and_left, mem_inter, mem_product]

Cartesian Product Distributes over Intersection: $s \times (t \cap t') = (s \times t) \cap (s \times t')$

Informal description

For any finite sets $s$ of type $\alpha$ and $t, t'$ of type $\beta$, the Cartesian product $s \times (t \cap t')$ is equal to $(s \times t) \cap (s \times t')$.

Finset.product_inter_product theorem

[DecidableEq α] [DecidableEq β] : s ×ˢ t ∩ s' ×ˢ t' = (s ∩ s') ×ˢ (t ∩ t')

Full source

theorem product_inter_product [DecidableEq α] [DecidableEq β] :
    s ×ˢ t ∩ s' ×ˢ t' = (s ∩ s') ×ˢ (t ∩ t') := by
  ext ⟨x, y⟩
  simp only [and_assoc, and_left_comm, mem_inter, mem_product]

Intersection of Cartesian Products Equals Cartesian Product of Intersections

Informal description

For any finite sets $s, s' \subseteq \alpha$ and $t, t' \subseteq \beta$, the intersection of the Cartesian products $s \times t$ and $s' \times t'$ is equal to the Cartesian product of the intersections $(s \cap s') \times (t \cap t')$. Here, $\times$ denotes the Cartesian product of sets, and $\cap$ denotes set intersection.

Finset.disjoint_product theorem

: Disjoint (s ×ˢ t) (s' ×ˢ t') ↔ Disjoint s s' ∨ Disjoint t t'

Full source

theorem disjoint_product : DisjointDisjoint (s ×ˢ t) (s' ×ˢ t') ↔ Disjoint s s' ∨ Disjoint t t' := by
  simp_rw [← disjoint_coe, coe_product, Set.disjoint_prod]

Disjointness of Cartesian Products: $s \times t \cap s' \times t' = \emptyset \iff s \cap s' = \emptyset \lor t \cap t' = \emptyset$

Informal description

For any finite sets $s, s' \subseteq \alpha$ and $t, t' \subseteq \beta$, the Cartesian products $s \times t$ and $s' \times t'$ are disjoint if and only if either $s$ and $s'$ are disjoint or $t$ and $t'$ are disjoint.

Finset.disjUnion_product theorem

(hs : Disjoint s s') : s.disjUnion s' hs ×ˢ t = (s ×ˢ t).disjUnion (s' ×ˢ t) (disjoint_product.mpr <| Or.inl hs)

Full source

@[simp]
theorem disjUnion_product (hs : Disjoint s s') :
    s.disjUnion s' hs ×ˢ t = (s ×ˢ t).disjUnion (s' ×ˢ t) (disjoint_product.mpr <| Or.inl hs) :=
  eq_of_veq <| Multiset.add_product _ _ _

Distributivity of Cartesian Product over Disjoint Union: $(s \sqcup s') \times t = (s \times t) \sqcup (s' \times t)$

Informal description

For any finite sets $s, s' \subseteq \alpha$ and $t \subseteq \beta$, if $s$ and $s'$ are disjoint, then the Cartesian product of their disjoint union with $t$ is equal to the disjoint union of the Cartesian products $s \times t$ and $s' \times t$. That is, \[ (s \sqcup s') \times t = (s \times t) \sqcup (s' \times t), \] where $\sqcup$ denotes the disjoint union operation.

Finset.product_disjUnion theorem

(ht : Disjoint t t') : s ×ˢ t.disjUnion t' ht = (s ×ˢ t).disjUnion (s ×ˢ t') (disjoint_product.mpr <| Or.inr ht)

Full source

@[simp]
theorem product_disjUnion (ht : Disjoint t t') :
    s ×ˢ t.disjUnion t' ht = (s ×ˢ t).disjUnion (s ×ˢ t') (disjoint_product.mpr <| Or.inr ht) :=
  eq_of_veq <| Multiset.product_add _ _ _

Distributivity of Cartesian Product over Disjoint Union (Right)

Informal description

For any finite sets $s \subseteq \alpha$, $t \subseteq \beta$, and $t' \subseteq \beta$ such that $t$ and $t'$ are disjoint, the Cartesian product of $s$ with the disjoint union of $t$ and $t'$ is equal to the disjoint union of the Cartesian products $s \times t$ and $s \times t'$. That is, \[ s \times (t \sqcup t') = (s \times t) \sqcup (s \times t'). \]

Finset.diag definition

Full source

/-- Given a finite set `s`, the diagonal, `s.diag` is the set of pairs of the form `(a, a)` for
`a ∈ s`. -/
def diag :=
  (s ×ˢ s).filter fun a : α × α => a.fst = a.snd

Diagonal of a finite set

Informal description

Given a finite set $ s $ of elements of type $ \alpha $, the diagonal $ s.\text{diag} $ is the finite subset of $ \alpha \times \alpha $ consisting of all pairs $ (a, a) $ where $ a \in s $. In other words, it is the set of elements in the Cartesian product $ s \times s $ filtered to include only those pairs where the first and second components are equal.

Finset.offDiag definition

Full source

/-- Given a finite set `s`, the off-diagonal, `s.offDiag` is the set of pairs `(a, b)` with `a ≠ b`
for `a, b ∈ s`. -/
def offDiag :=
  (s ×ˢ s).filter fun a : α × α => a.fst ≠ a.snd

Off-diagonal of a finite set

Informal description

Given a finite set $s$ of type $\alpha$, the off-diagonal $s.\text{offDiag}$ is the finite subset of $\alpha \times \alpha$ consisting of all pairs $(a, b)$ where $a, b \in s$ and $a \neq b$.

Finset.mem_diag theorem

: x ∈ s.diag ↔ x.1 ∈ s ∧ x.1 = x.2

Full source

@[simp]
theorem mem_diag : x ∈ s.diagx ∈ s.diag ↔ x.1 ∈ s ∧ x.1 = x.2 := by
  simp +contextual [diag]

Membership in Diagonal of Finite Set

Informal description

For any element $x$ in the product type $\alpha \times \alpha$ and any finite set $s$ of type $\alpha$, the element $x$ belongs to the diagonal of $s$ if and only if the first component of $x$ is in $s$ and the two components of $x$ are equal, i.e., $x = (a, a)$ for some $a \in s$.

Finset.mem_offDiag theorem

: x ∈ s.offDiag ↔ x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2

Full source

@[simp]
theorem mem_offDiag : x ∈ s.offDiagx ∈ s.offDiag ↔ x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2 := by
  simp [offDiag, and_assoc]

Membership in the Off-Diagonal of a Finite Set

Informal description

For any element $x = (a, b)$ in the type $\alpha \times \alpha$ and any finite set $s$ of type $\alpha$, the element $x$ belongs to the off-diagonal of $s$ if and only if both $a$ and $b$ are elements of $s$ and $a \neq b$. In other words, $x \in s.\text{offDiag} \leftrightarrow a \in s \land b \in s \land a \neq b$.

Finset.coe_offDiag theorem

: (s.offDiag : Set (α × α)) = (s : Set α).offDiag

Full source

@[simp, norm_cast]
theorem coe_offDiag : (s.offDiag : Set (α × α)) = (s : Set α).offDiag :=
  Set.ext fun _ => mem_offDiag

Equality of Finite Set Off-Diagonal and Set Off-Diagonal

Informal description

For any finite set $s$ of type $\alpha$, the underlying set of the off-diagonal $s.\text{offDiag}$ is equal to the off-diagonal of the underlying set of $s$. That is, $(s.\text{offDiag} : \text{Set} (\alpha \times \alpha)) = (s : \text{Set} \alpha).\text{offDiag}$.

Finset.diag_card theorem

: (diag s).card = s.card

Full source

@[simp]
theorem diag_card : (diag s).card = s.card := by
  suffices diag s = s.image fun a => (a, a) by
    rw [this]
    apply card_image_of_injOn
    exact fun x1 _ x2 _ h3 => (Prod.mk.inj h3).1
  ext ⟨a₁, a₂⟩
  rw [mem_diag]
  constructor <;> intro h <;> rw [Finset.mem_image] at *
  · use a₁
    simpa using h
  · rcases h with ⟨a, h1, h2⟩
    have h := Prod.mk.inj h2
    rw [← h.1, ← h.2]
    use h1

Cardinality of Diagonal Set Equals Cardinality of Original Set

Informal description

For any finite set $s$ of type $\alpha$, the cardinality of the diagonal set $s.\text{diag}$ is equal to the cardinality of $s$. In other words, $|s.\text{diag}| = |s|$.

Finset.offDiag_card theorem

: (offDiag s).card = s.card * s.card - s.card

Full source

@[simp]
theorem offDiag_card : (offDiag s).card = s.card * s.card - s.card :=
  suffices (diag s).card + (offDiag s).card = s.card * s.card by rw [s.diag_card] at this; omega
  by rw [← card_product, diag, offDiag]
     conv_rhs => rw [← filter_card_add_filter_neg_card_eq_card (fun a => a.1 = a.2)]

Cardinality of Off-Diagonal Set: $|\text{offDiag}(s)| = |s|^2 - |s|$

Informal description

For any finite set $s$ of type $\alpha$, the cardinality of the off-diagonal set $s.\text{offDiag}$ is equal to $|s|^2 - |s|$, where $|s|$ denotes the cardinality of $s$.

Finset.diag_mono theorem

: Monotone (diag : Finset α → Finset (α × α))

Full source

@[mono]
theorem diag_mono : Monotone (diag : Finset α → Finset (α × α)) := fun _ _ h _ hx =>
  mem_diag.2 <| And.imp_left (@h _) <| mem_diag.1 hx

Monotonicity of the Diagonal Map on Finite Sets

Informal description

The function $\text{diag} : \text{Finset} \alpha \to \text{Finset} (\alpha \times \alpha)$, which maps a finite set $s$ to its diagonal $\{(a, a) \mid a \in s\}$, is monotone. That is, for any finite sets $s, t \subseteq \alpha$, if $s \subseteq t$, then $\text{diag}(s) \subseteq \text{diag}(t)$.

Finset.offDiag_mono theorem

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

Full source

@[mono]
theorem offDiag_mono : Monotone (offDiag : Finset α → Finset (α × α)) := fun _ _ h _ hx =>
  mem_offDiag.2 <| And.imp (@h _) (And.imp_left <| @h _) <| mem_offDiag.1 hx

Monotonicity of the Off-Diagonal Map on Finite Sets

Informal description

The function $\text{offDiag} : \text{Finset} \alpha \to \text{Finset} (\alpha \times \alpha)$, which maps a finite set $s$ to its off-diagonal $\{(a, b) \mid a, b \in s \text{ and } a \neq b\}$, is monotone. That is, for any finite sets $s, t \subseteq \alpha$, if $s \subseteq t$, then $\text{offDiag}(s) \subseteq \text{offDiag}(t)$.

Finset.diag_empty theorem

: (∅ : Finset α).diag = ∅

Full source

@[simp]
theorem diag_empty : (∅ : Finset α).diag = ∅ :=
  rfl

Diagonal of Empty Finset is Empty

Informal description

The diagonal of the empty finset is empty, i.e., $\text{diag}(\emptyset) = \emptyset$.

Finset.offDiag_empty theorem

: (∅ : Finset α).offDiag = ∅

Full source

@[simp]
theorem offDiag_empty : (∅ : Finset α).offDiag = ∅ :=
  rfl

Empty Set's Off-Diagonal is Empty

Informal description

The off-diagonal of the empty finite set is empty, i.e., $\emptyset.\text{offDiag} = \emptyset$.

Finset.diag_union_offDiag theorem

: s.diag ∪ s.offDiag = s ×ˢ s

Full source

@[simp]
theorem diag_union_offDiag : s.diag ∪ s.offDiag = s ×ˢ s := by
  conv_rhs => rw [← filter_union_filter_neg_eq (fun a => a.1 = a.2) (s ×ˢ s)]
  rfl

Union of Diagonal and Off-Diagonal Equals Cartesian Square of Finite Set

Informal description

For any finite set $s$ of type $\alpha$, the union of the diagonal $s.\text{diag}$ (consisting of pairs $(a,a)$ with $a \in s$) and the off-diagonal $s.\text{offDiag}$ (consisting of pairs $(a,b)$ with $a, b \in s$ and $a \neq b$) equals the Cartesian product $s \times s$.

Finset.disjoint_diag_offDiag theorem

: Disjoint s.diag s.offDiag

Full source

@[simp]
theorem disjoint_diag_offDiag : Disjoint s.diag s.offDiag :=
  disjoint_filter_filter_neg (s ×ˢ s) (s ×ˢ s) (fun a => a.1 = a.2)

Disjointness of Diagonal and Off-Diagonal in Finite Sets

Informal description

For any finite set $s$ of type $\alpha$, the diagonal $s.\text{diag}$ and the off-diagonal $s.\text{offDiag}$ are disjoint subsets of $s \times s$. That is, there is no pair $(a, b)$ that belongs to both the diagonal and the off-diagonal of $s$.

Finset.product_sdiff_diag theorem

: s ×ˢ s \ s.diag = s.offDiag

Full source

theorem product_sdiff_diag : s ×ˢ s \ s.diag = s.offDiag := by
  rw [← diag_union_offDiag, union_comm, union_sdiff_self,
    sdiff_eq_self_of_disjoint (disjoint_diag_offDiag _).symm]

Set Difference of Cartesian Square and Diagonal Equals Off-Diagonal: $(s \times s) \setminus \text{diag}(s) = \text{offDiag}(s)$

Informal description

For any finite set $s$ of type $\alpha$, the set difference between the Cartesian product $s \times s$ and the diagonal $s.\text{diag}$ equals the off-diagonal $s.\text{offDiag}$. In other words, $(s \times s) \setminus \{(a, a) \mid a \in s\} = \{(a, b) \mid a, b \in s, a \neq b\}$.

Finset.product_sdiff_offDiag theorem

: s ×ˢ s \ s.offDiag = s.diag

Full source

theorem product_sdiff_offDiag : s ×ˢ s \ s.offDiag = s.diag := by
  rw [← diag_union_offDiag, union_sdiff_self, sdiff_eq_self_of_disjoint (disjoint_diag_offDiag _)]

Set Difference of Cartesian Square and Off-Diagonal Equals Diagonal: $(s \times s) \setminus \text{offDiag}(s) = \text{diag}(s)$

Informal description

For any finite set $s$ of type $\alpha$, the set difference between the Cartesian product $s \times s$ and the off-diagonal $s.\text{offDiag}$ equals the diagonal $s.\text{diag}$. In other words, $(s \times s) \setminus \text{offDiag}(s) = \text{diag}(s)$.

Finset.diag_inter theorem

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

Full source

theorem diag_inter : (s ∩ t).diag = s.diag ∩ t.diag :=
  ext fun x => by simpa only [mem_diag, mem_inter] using and_and_right

Diagonal of Intersection Equals Intersection of Diagonals

Informal description

For any two finite sets $s$ and $t$ of elements of type $\alpha$, the diagonal of their intersection $(s \cap t).\text{diag}$ is equal to the intersection of their diagonals $s.\text{diag} \cap t.\text{diag}$.

Finset.offDiag_inter theorem

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

Full source

theorem offDiag_inter : (s ∩ t).offDiag = s.offDiag ∩ t.offDiag :=
  coe_injective <| by
    push_cast
    exact Set.offDiag_inter _ _

Intersection of Off-Diagonals Equals Off-Diagonal of Intersection for Finite Sets

Informal description

For any two finite sets $s$ and $t$ of elements of type $\alpha$, the off-diagonal of their intersection $(s \cap t).\text{offDiag}$ is equal to the intersection of their off-diagonals $s.\text{offDiag} \cap t.\text{offDiag}$. Here, the off-diagonal consists of all pairs $(a, b)$ with $a, b \in s$ (or $t$) and $a \neq b$.

Finset.diag_union theorem

: (s ∪ t).diag = s.diag ∪ t.diag

Full source

theorem diag_union : (s ∪ t).diag = s.diag ∪ t.diag := by
  ext ⟨i, j⟩
  simp only [mem_diag, mem_union, or_and_right]

Union of Diagonals Equals Diagonal of Union for Finite Sets

Informal description

For any two finite sets $s$ and $t$ of elements of type $\alpha$, the diagonal of their union $(s \cup t).\text{diag}$ is equal to the union of their diagonals $s.\text{diag} \cup t.\text{diag}$. In other words, the set of pairs $(a, a)$ where $a \in s \cup t$ is exactly the union of the sets of pairs $(a, a)$ where $a \in s$ and $(a, a)$ where $a \in t$.

Finset.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 :=
  coe_injective <| by
    push_cast
    exact Set.offDiag_union (disjoint_coe.2 h)

Off-diagonal of Union of Disjoint Finite Sets

Informal description

For any two disjoint finite sets $s$ and $t$ of type $\alpha$, the off-diagonal of their union $(s \cup t).\text{offDiag}$ is equal to the union of their individual 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).$$

Finset.offDiag_singleton theorem

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

Full source

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

Off-diagonal of Singleton is Empty

Informal description

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

Finset.diag_singleton theorem

: ({ a } : Finset α).diag = {(a, a)}

Full source

theorem diag_singleton : ({a} : Finset α).diag = {(a, a)} := by
  rw [← product_sdiff_offDiag, offDiag_singleton, sdiff_empty, singleton_product_singleton]

Diagonal of Singleton: $\text{diag}(\{a\}) = \{(a, a)\}$

Informal description

For any element $a$ of type $\alpha$, the diagonal of the singleton finite set $\{a\}$ is the set $\{(a, a)\}$.

Finset.diag_insert theorem

: (insert a s).diag = insert (a, a) s.diag

Full source

theorem diag_insert : (insert a s).diag = insert (a, a) s.diag := by
  rw [insert_eq, insert_eq, diag_union, diag_singleton]

Diagonal of Inserted Element in Finite Set: $\text{diag}(\{a\} \cup s) = \{(a,a)\} \cup \text{diag}(s)$

Informal description

For any element $a$ of type $\alpha$ and any finite set $s$ of elements of $\alpha$, the diagonal of the set obtained by inserting $a$ into $s$ is equal to the insertion of the pair $(a, a)$ into the diagonal of $s$. That is, $$\text{diag}(\text{insert } a s) = \text{insert } (a, a) (\text{diag } s).$$

Finset.offDiag_insert theorem

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

Full source

theorem offDiag_insert (has : a ∉ s) : (insert a s).offDiag = s.offDiag ∪ {a} ×ˢ ss.offDiag ∪ {a} ×ˢ s ∪ s ×ˢ {a} := by
  rw [insert_eq, union_comm, offDiag_union (disjoint_singleton_right.2 has), offDiag_singleton,
    union_empty, union_right_comm]

Off-diagonal of Inserted Element in Finite Set

Informal description

For any element $a$ not in a finite set $s$ of 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$, the Cartesian product of $\{a\}$ with $s$, and the Cartesian product of $s$ with $\{a\}$. That is, $$(\text{insert } a s).\text{offDiag} = s.\text{offDiag} \cup (\{a\} \times s) \cup (s \times \{a\}).$$

Finset.offDiag_filter_lt_eq_filter_le theorem

 {ι} [PartialOrder ι] [DecidableEq ι] [DecidableLE ι] [DecidableLT ι] (s : Finset ι) :
  s.offDiag.filter (fun i => i.1 < i.2) = s.offDiag.filter (fun i => i.1 ≤ i.2)

Full source

theorem offDiag_filter_lt_eq_filter_le {ι} [PartialOrder ι]
    [DecidableEq ι] [DecidableLE ι] [DecidableLT ι] (s : Finset ι) :
    s.offDiag.filter (fun i => i.1 < i.2) = s.offDiag.filter (fun i => i.1 ≤ i.2) := by
  rw [Finset.filter_inj']
  rintro ⟨i, j⟩
  simp_rw [mem_offDiag, and_imp]
  rintro _ _ h
  rw [Ne.le_iff_lt h]

Equality of Filtered Off-Diagonal Pairs in Partial Order: $i < j$ iff $i \leq j$

Informal description

For a finite set $s$ of elements in a partially ordered type $\iota$ with decidable equality, order, and strict order, the filtered subset of the off-diagonal pairs $(i, j) \in s \times s$ with $i < j$ is equal to the filtered subset of off-diagonal pairs with $i \leq j$.

Main declarations