Set.IsPWO.add
theorem Set.IsPWO.add :
∀ {α : Type u_1} {s t : Set α} [inst : OrderedCancelAddCommMonoid α], s.IsPWO → t.IsPWO → (s + t).IsPWO
This theorem states that for any two sets `s` and `t` of an ordered cancellative commutative monoid `α`, if both sets are partially well-ordered (PWO), then their sum set (the set of all elements that can be written as the sum of an element from `s` and an element from `t`) is also partially well-ordered. Being partially well-ordered means that any infinite sequence from the set contains a monotone subsequence of length 2, or equivalently, an infinite monotone subsequence. In the context of an ordered cancellative commutative monoid, monotone refers to the partial order defined by the monoid operation.
More concisely: In an ordered cancellative commutative monoid, if two partially well-ordered sets have the property that any infinite sequence contains a monotonic subsequence of length 2 using the monoid operation, then their sum set is also partially well-ordered.
|
Mathlib.Data.Finset.MulAntidiagonal._auxLemma.4
theorem Mathlib.Data.Finset.MulAntidiagonal._auxLemma.4 :
∀ {α : Type u_1} [inst : OrderedCancelAddCommMonoid α] {s t : Set α} {hs : s.IsPWO} {ht : t.IsPWO} {a : α}
{x : α × α}, (x ∈ Finset.addAntidiagonal hs ht a) = (x.1 ∈ s ∧ x.2 ∈ t ∧ x.1 + x.2 = a)
This theorem states that for any type `α` which has an `OrderedCancelAddCommMonoid` structure, given two partially well-ordered sets `s` and `t`, and an element `a` of type `α`, for any pair `x` of type `α × α`, `x` belongs to the set `Finset.addAntidiagonal hs ht a` if and only if the first element of `x` is in `s`, the second element of `x` is in `t`, and the sum of the elements of `x` equals `a`. In other words, `Finset.addAntidiagonal hs ht a` consists exactly of pairs whose elements are from `s` and `t` respectively and sum up to `a`.
More concisely: For any `OrderedCancelAddCommMonoid` type `α`, `Finset.addAntidiagonal` returns the set of pairs `(x, y)` from `α × α` such that `x ∈ s`, `y ∈ t`, and `x + y = a`.
|