Multiplication antidiagonal as a Finset.

We construct the Finset of all pairs of an element in s and an element in t that multiply to a, given that s and t are well-ordered.

theorem Set.IsPWO.add {α : Type u_1} {s : Set α} {t : Set α} [OrderedCancelAddCommMonoid α] (hs : Set.IsPWO s) (ht : Set.IsPWO t) : Set.IsPWO (s + t)

theorem Set.IsPWO.mul {α : Type u_1} {s : Set α} {t : Set α} [OrderedCancelCommMonoid α] (hs : Set.IsPWO s) (ht : Set.IsPWO t) : Set.IsPWO (s * t)

theorem Set.IsWF.add {α : Type u_1} {s : Set α} {t : Set α} [LinearOrderedCancelAddCommMonoid α] (hs : Set.IsWF s) (ht : Set.IsWF t) : Set.IsWF (s + t)

theorem Set.IsWF.mul {α : Type u_1} {s : Set α} {t : Set α} [LinearOrderedCancelCommMonoid α] (hs : Set.IsWF s) (ht : Set.IsWF t) : Set.IsWF (s * t)

theorem Set.IsWF.min_add {α : Type u_1} {s : Set α} {t : Set α} [LinearOrderedCancelAddCommMonoid α] (hs : Set.IsWF s) (ht : Set.IsWF t) (hsn : Set.Nonempty s) (htn : Set.Nonempty t) : Set.IsWF.min (_ : Set.IsWF (s + t)) (_ : Set.Nonempty (s + t)) = Set.IsWF.min hs hsn + Set.IsWF.min ht htn

theorem Set.IsWF.min_mul {α : Type u_1} {s : Set α} {t : Set α} [LinearOrderedCancelCommMonoid α] (hs : Set.IsWF s) (ht : Set.IsWF t) (hsn : Set.Nonempty s) (htn : Set.Nonempty t) : Set.IsWF.min (_ : Set.IsWF (s * t)) (_ : Set.Nonempty (s * t)) = Set.IsWF.min hs hsn * Set.IsWF.min ht htn

noncomputable def Finset.addAntidiagonal {α : Type u_1} [OrderedCancelAddCommMonoid α] {s : Set α} {t : Set α} (hs : Set.IsPWO s) (ht : Set.IsPWO t) (a : α) : Finset (α × α)

Finset.addAntidiagonal hs ht a is the set of all pairs of an element in s and an element in t that add to a, but its construction requires proofs that s and t are well-ordered.

Equations

• Finset.addAntidiagonal hs ht a = Set.Finite.toFinset (_ : Set.Finite (Set.addAntidiagonal s t a))

noncomputable def Finset.mulAntidiagonal {α : Type u_1} [OrderedCancelCommMonoid α] {s : Set α} {t : Set α} (hs : Set.IsPWO s) (ht : Set.IsPWO t) (a : α) : Finset (α × α)

Finset.mulAntidiagonal hs ht a is the set of all pairs of an element in s and an element in t that multiply to a, but its construction requires proofs that s and t are well-ordered.

Equations

• Finset.mulAntidiagonal hs ht a = Set.Finite.toFinset (_ : Set.Finite (Set.mulAntidiagonal s t a))

@[simp]

theorem Finset.mem_addAntidiagonal {α : Type u_1} [OrderedCancelAddCommMonoid α] {s : Set α} {t : Set α} {hs : Set.IsPWO s} {ht : Set.IsPWO t} {a : α} {x : α × α} : x ∈ Finset.addAntidiagonal hs ht a ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ x.1 + x.2 = a

@[simp]

theorem Finset.mem_mulAntidiagonal {α : Type u_1} [OrderedCancelCommMonoid α] {s : Set α} {t : Set α} {hs : Set.IsPWO s} {ht : Set.IsPWO t} {a : α} {x : α × α} : x ∈ Finset.mulAntidiagonal hs ht a ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ x.1 * x.2 = a

theorem Finset.addAntidiagonal_mono_left {α : Type u_1} [OrderedCancelAddCommMonoid α] {s : Set α} {t : Set α} {hs : Set.IsPWO s} {ht : Set.IsPWO t} {a : α} {u : Set α} {hu : Set.IsPWO u} (h : u ⊆ s) : Finset.addAntidiagonal hu ht a ⊆ Finset.addAntidiagonal hs ht a

theorem Finset.mulAntidiagonal_mono_left {α : Type u_1} [OrderedCancelCommMonoid α] {s : Set α} {t : Set α} {hs : Set.IsPWO s} {ht : Set.IsPWO t} {a : α} {u : Set α} {hu : Set.IsPWO u} (h : u ⊆ s) : Finset.mulAntidiagonal hu ht a ⊆ Finset.mulAntidiagonal hs ht a

theorem Finset.addAntidiagonal_mono_right {α : Type u_1} [OrderedCancelAddCommMonoid α] {s : Set α} {t : Set α} {hs : Set.IsPWO s} {ht : Set.IsPWO t} {a : α} {u : Set α} {hu : Set.IsPWO u} (h : u ⊆ t) : Finset.addAntidiagonal hs hu a ⊆ Finset.addAntidiagonal hs ht a

theorem Finset.mulAntidiagonal_mono_right {α : Type u_1} [OrderedCancelCommMonoid α] {s : Set α} {t : Set α} {hs : Set.IsPWO s} {ht : Set.IsPWO t} {a : α} {u : Set α} {hu : Set.IsPWO u} (h : u ⊆ t) : Finset.mulAntidiagonal hs hu a ⊆ Finset.mulAntidiagonal hs ht a

theorem Finset.swap_mem_addAntidiagonal {α : Type u_1} [OrderedCancelAddCommMonoid α] {s : Set α} {t : Set α} {hs : Set.IsPWO s} {ht : Set.IsPWO t} {a : α} {x : α × α} : Prod.swap x ∈ Finset.addAntidiagonal hs ht a ↔ x ∈ Finset.addAntidiagonal ht hs a

theorem Finset.swap_mem_mulAntidiagonal {α : Type u_1} [OrderedCancelCommMonoid α] {s : Set α} {t : Set α} {hs : Set.IsPWO s} {ht : Set.IsPWO t} {a : α} {x : α × α} : Prod.swap x ∈ Finset.mulAntidiagonal hs ht a ↔ x ∈ Finset.mulAntidiagonal ht hs a

theorem Finset.support_addAntidiagonal_subset_add {α : Type u_1} [OrderedCancelAddCommMonoid α] {s : Set α} {t : Set α} {hs : Set.IsPWO s} {ht : Set.IsPWO t} : {a : α | (Finset.addAntidiagonal hs ht a).Nonempty} ⊆ s + t

abbrev Finset.support_addAntidiagonal_subset_add.match_1 {α : Type u_1} [OrderedCancelAddCommMonoid α] {s : Set α} {t : Set α} {hs : Set.IsPWO s} {ht : Set.IsPWO t} (a : α) (motive : a ∈ {a : α | (Finset.addAntidiagonal hs ht a).Nonempty} → Prop) : ∀ (x : a ∈ {a : α | (Finset.addAntidiagonal hs ht a).Nonempty}), (∀ (b : α × α) (hb : b ∈ Finset.addAntidiagonal hs ht a), motive (_ : ∃ (x : α × α), x ∈ Finset.addAntidiagonal hs ht a)) → motive x

Equations

• (_ : motive x) = (_ : motive x)

theorem Finset.support_mulAntidiagonal_subset_mul {α : Type u_1} [OrderedCancelCommMonoid α] {s : Set α} {t : Set α} {hs : Set.IsPWO s} {ht : Set.IsPWO t} : {a : α | (Finset.mulAntidiagonal hs ht a).Nonempty} ⊆ s * t

theorem Finset.isPWO_support_addAntidiagonal {α : Type u_1} [OrderedCancelAddCommMonoid α] {s : Set α} {t : Set α} {hs : Set.IsPWO s} {ht : Set.IsPWO t} : Set.IsPWO {a : α | (Finset.addAntidiagonal hs ht a).Nonempty}

theorem Finset.isPWO_support_mulAntidiagonal {α : Type u_1} [OrderedCancelCommMonoid α] {s : Set α} {t : Set α} {hs : Set.IsPWO s} {ht : Set.IsPWO t} : Set.IsPWO {a : α | (Finset.mulAntidiagonal hs ht a).Nonempty}

theorem Finset.addAntidiagonal_min_add_min {α : Type u_2} [LinearOrderedCancelAddCommMonoid α] {s : Set α} {t : Set α} (hs : Set.IsWF s) (ht : Set.IsWF t) (hns : Set.Nonempty s) (hnt : Set.Nonempty t) : Finset.addAntidiagonal (_ : Set.IsPWO s) (_ : Set.IsPWO t) (Set.IsWF.min hs hns + Set.IsWF.min ht hnt) = {(Set.IsWF.min hs hns, Set.IsWF.min ht hnt)}

theorem Finset.mulAntidiagonal_min_mul_min {α : Type u_2} [LinearOrderedCancelCommMonoid α] {s : Set α} {t : Set α} (hs : Set.IsWF s) (ht : Set.IsWF t) (hns : Set.Nonempty s) (hnt : Set.Nonempty t) : Finset.mulAntidiagonal (_ : Set.IsPWO s) (_ : Set.IsPWO t) (Set.IsWF.min hs hns * Set.IsWF.min ht hnt) = {(Set.IsWF.min hs hns, Set.IsWF.min ht hnt)}