Set.image_add_const_Icc
theorem Set.image_add_const_Icc :
∀ {M : Type u_1} [inst : OrderedCancelAddCommMonoid M] [inst_1 : ExistsAddOfLE M] (a b c : M),
(fun x => x + a) '' Set.Icc b c = Set.Icc (b + a) (c + a)
This theorem states that for any ordered cancelable commutative monoid `M` where addition exists for less than or equal elements, and given any elements `a`, `b`, and `c` of type `M`, the image of the interval from `b` to `c` (inclusive at both ends, denoted as `Set.Icc b c`) under the function `x ⟼ x + a` is exactly the interval from `b + a` to `c + a` (again inclusive at both ends). This is essentially a translation of the interval `[b, c]` by `a` along the real line.
More concisely: For any ordered cancelable commutative monoid `M` with addition, and elements `a`, `b`, and `c` of `M`, the image of the interval `Set.Icc b c` under the function `x ⟼ x + a` equals `Set.Icc (b + a) (c + a)`.
|
Set.Ici_add_bij
theorem Set.Ici_add_bij :
∀ {M : Type u_1} [inst : OrderedCancelAddCommMonoid M] [inst_1 : ExistsAddOfLE M] (a d : M),
Set.BijOn (fun x => x + d) (Set.Ici a) (Set.Ici (a + d))
This theorem, `Set.Ici_add_bij`, states that for any type `M` that is an ordered, cancelable, and commutative monoid with an existing additive order (i.e., for every pair of elements in `M`, there exists a third element such that adding it to the lesser element yields the greater element), and for any two elements `a` and `d` of `M`, the function that adds `d` to an input is a bijective function from the set of elements that are greater than or equal to `a` (`Set.Ici a`) to the set of elements that are greater than or equal to `a + d` (`Set.Ici (a + d)`). In other words, if we add `d` to each element in the left-closed right-infinite interval starting at `a`, we get a one-to-one correspondence with the left-closed right-infinite interval starting at `a + d`.
More concisely: For any ordered, cancelable, and commutative monoid `M` with an additive order, the function that adds a fixed element `d` is a bijection from the set of elements greater than or equal to `a` to the set of elements greater than or equal to `a + d`.
|
Set.Ioi_add_bij
theorem Set.Ioi_add_bij :
∀ {M : Type u_1} [inst : OrderedCancelAddCommMonoid M] [inst_1 : ExistsAddOfLE M] (a d : M),
Set.BijOn (fun x => x + d) (Set.Ioi a) (Set.Ioi (a + d))
This theorem states that for any type `M` that is an ordered, cancellative, commutative monoid and has a property that for all `a` and `b` in `M`, if `a ≤ b` then there exists `c` in `M` such that `b = a + c`, and for any elements `a` and `d` in `M`, the function `f(x) = x + d` is a bijection from the set of all elements of `M` that are greater than `a` to the set of all elements of `M` that are greater than `a + d`. In other words, adding `d` to each element in the open interval `(a, ∞)` in `M` results in a one-to-one and onto mapping to the open interval `(a+d, ∞)` in `M`.
More concisely: For any ordered, cancellative, commutative monoid `M` with the property that for all `a` and `b` in `M` with `a ≤ b` there exists `c` in `M` such that `b = a + c`, the function `f(x) = x + d` is a bijection between the sets `{x in M | x > a}` and `{x in M | x > a + d}`.
|