disjoint_disjointed
theorem disjoint_disjointed :
∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] (f : ℕ → α), Pairwise (Disjoint on disjointed f)
The theorem `disjoint_disjointed` states that for any sequence `f` of elements of type `α` in a generalized boolean algebra, the `disjointed` sequence derived from `f` is pairwise disjoint. Here, a sequence `f` is `disjointed` by subtracting each element from its successors, and two elements are considered disjoint if their infimum (greatest lower bound) is the bottom element of the lattice. This theorem thus asserts that any two distinct elements of the `disjointed` sequence have an infimum of the bottom element, which implies that the elements of the `disjointed` sequence are pairwise disjoint.
More concisely: In a generalized boolean algebra, any two distinct elements in a sequence obtained by subtracting each element from its successors (i.e., the `disjointed` sequence) have infimum equal to the bottom element, implying they are pairwise disjoint.
|
disjointed_unique
theorem disjointed_unique :
∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] {f d : ℕ → α},
Pairwise (Disjoint on d) → partialSups d = partialSups f → d = disjointed f
The theorem `disjointed_unique` states that for any sequence `f` and `d` from natural numbers to an object `α` of a generalized Boolean algebra, if `d` is pairwise disjoint (every two distinct elements are disjoint) and the sequence of partial supremums of `d` is the same as that of `f`, then `d` is equal to the sequence `disjointed f`. The sequence `disjointed f` is defined as the sequence formed by subtracting each element of `f` from its successors, and it is the unique sequence that is pairwise disjoint and whose sequence of partial supremums is the same as `f`.
More concisely: If `d` is a pairwise disjoint sequence of natural numbers to an object `α` in a generalized Boolean algebra with the same sequence of partial supremums as `f`, then `d` equals the sequence `disjointed f`.
|
disjointed_subset
theorem disjointed_subset : ∀ {α : Type u_1} (f : ℕ → Set α) (n : ℕ), disjointed f n ⊆ f n
This theorem states that for any type `α` and any function `f` from natural numbers `ℕ` to the set of `α`, the `n-th` term of the disjointed sequence of `f` is a subset of the `n-th` term of the original sequence `f`. Here, the disjointed sequence is computed by subtracting each element from the subsequent elements, producing a sequence with the same partial supremums as the original sequence. The subset relation `⊆` indicates that every element of the disjointed sequence at the `n-th` position is also an element of the original sequence at the same position.
More concisely: For any type `α` and function `f : ℕ → α`, the sequence obtained by subtracting successive terms of `f` is a subset of the original sequence `f`.
|
iUnion_disjointed
theorem iUnion_disjointed : ∀ {α : Type u_1} {f : ℕ → Set α}, ⋃ n, disjointed f n = ⋃ n, f n
The theorem `iUnion_disjointed` states that for any type `α` and any sequence of sets `f : ℕ → Set α`, the union over `n` of the disjointed form of `f` equals the union over `n` of `f` itself. In other words, if `f` is a sequence of sets, and `disjointed f` is the sequence formed by subtracting each set from the next ones in the sequence, then the union of all sets in the disjointed sequence is the same as the union of all sets in the original sequence.
More concisely: For any sequence of sets `f : ℕ → Set α`, the union of the disjointed sequence `disjointed f` equals the union of `f`.
|
disjointed_le
theorem disjointed_le : ∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] (f : ℕ → α), disjointed f ≤ f
The theorem `disjointed_le` states that for any sequence `f : ℕ → α` in a generalized boolean algebra `α`, the sequence `disjointed f`, which is formed by subtracting each element from its successors, is less than or equal to the original sequence `f`. This is expressed in terms of the lattice order defined by the generalized boolean algebra structure.
More concisely: For any sequence in a generalized boolean algebra, the sequence obtained by subtracting each element from its successor is less than or equal to the original sequence in the lattice order.
|