Set.nonempty_Ico_sdiff
theorem Set.nonempty_Ico_sdiff :
∀ {α : Type u_1} [inst : LinearOrderedAddCommGroup α] {x dx y dy : α},
dy < dx → 0 < dx → Nonempty ↑(Set.Ico x (x + dx) \ Set.Ico y (y + dy))
This theorem states that if we are given a type `α` which is a linearly ordered additive commutative group, along with elements `x`, `dx`, `y`, and `dy` of this type, then if `dy` is less than `dx` and `dx` is greater than zero, the set obtained by removing the left-closed right-open interval from `y` to `y + dy` from the left-closed right-open interval from `x` to `x + dx` is non-empty. In other words, there exists at least one element in the interval `[x, x + dx)` which is not in the interval `[y, y + dy)`.
More concisely: If `α` is a linearly ordered additive commutative group, `x, dx, y, dy` are elements of `α` with `dx > 0` and `dy < dx`, then there exists an element `z` in `[x, x + dx)` that is not in `[y, y + dy)`.
|
Set.pairwise_disjoint_Ioc_add_zsmul
theorem Set.pairwise_disjoint_Ioc_add_zsmul :
∀ {α : Type u_1} [inst : OrderedAddCommGroup α] (a b : α),
Pairwise (Disjoint on fun n => Set.Ioc (a + n • b) (a + (n + 1) • b))
The theorem `Set.pairwise_disjoint_Ioc_add_zsmul` states that for any type `α` which is an ordered additive commutative group, and for any two elements `a` and `b` of this type, we have that the left-open right-closed intervals `(a + n • b, a + (n + 1) • b]` are pairwise disjoint. In other words, for any two different integers `n` and `m`, there is no `x` which belongs to both intervals `(a + n • b, a + (n + 1) • b]` and `(a + m • b, a + (m + 1) • b]`. Here, `•` represents the scalar multiplication operation in the group, and `Disjoint` means that the infimum (greatest lower bound) of the two sets is the bottom element of the lattice of subsets.
More concisely: For any ordered additive commutative group type `α` and elements `a, b` in `α`, the left-open right-closed intervals `(a + n • b, a + (n + 1) • b]` are pairwise disjoint for distinct integers `n`.
|