Images of intervals under (+ d)

The lemmas in this file state that addition maps intervals bijectively. The typeclass ExistsAddOfLE is defined specifically to make them work when combined with IsOrderedCancelAddMonoid; the lemmas below therefore apply to all ordered groups, but also to ℕ and ℝ≥0, which are not groups.

theorem Set.Ici_add_bij {M : Type u_1} [AddCommMonoid M] [PartialOrder M] [IsOrderedCancelAddMonoid M] [ExistsAddOfLE M] (a d : M) : BijOn (fun (x : M) => x + d) (Ici a) (Ici (a + d))

theorem Set.Ioi_add_bij {M : Type u_1} [AddCommMonoid M] [PartialOrder M] [IsOrderedCancelAddMonoid M] [ExistsAddOfLE M] (a d : M) : BijOn (fun (x : M) => x + d) (Ioi a) (Ioi (a + d))

theorem Set.Icc_add_bij {M : Type u_1} [AddCommMonoid M] [PartialOrder M] [IsOrderedCancelAddMonoid M] [ExistsAddOfLE M] (a b d : M) : BijOn (fun (x : M) => x + d) (Icc a b) (Icc (a + d) (b + d))

theorem Set.Ioo_add_bij {M : Type u_1} [AddCommMonoid M] [PartialOrder M] [IsOrderedCancelAddMonoid M] [ExistsAddOfLE M] (a b d : M) : BijOn (fun (x : M) => x + d) (Ioo a b) (Ioo (a + d) (b + d))

theorem Set.Ioc_add_bij {M : Type u_1} [AddCommMonoid M] [PartialOrder M] [IsOrderedCancelAddMonoid M] [ExistsAddOfLE M] (a b d : M) : BijOn (fun (x : M) => x + d) (Ioc a b) (Ioc (a + d) (b + d))

theorem Set.Ico_add_bij {M : Type u_1} [AddCommMonoid M] [PartialOrder M] [IsOrderedCancelAddMonoid M] [ExistsAddOfLE M] (a b d : M) : BijOn (fun (x : M) => x + d) (Ico a b) (Ico (a + d) (b + d))

Images under x ↦ x + a

@[simp]

theorem Set.image_add_const_Ici {M : Type u_1} [AddCommMonoid M] [PartialOrder M] [IsOrderedCancelAddMonoid M] [ExistsAddOfLE M] (a b : M) : (fun (x : M) => x + a) '' Ici b = Ici (b + a)

@[simp]

theorem Set.image_add_const_Ioi {M : Type u_1} [AddCommMonoid M] [PartialOrder M] [IsOrderedCancelAddMonoid M] [ExistsAddOfLE M] (a b : M) : (fun (x : M) => x + a) '' Ioi b = Ioi (b + a)

@[simp]

theorem Set.image_add_const_Icc {M : Type u_1} [AddCommMonoid M] [PartialOrder M] [IsOrderedCancelAddMonoid M] [ExistsAddOfLE M] (a b c : M) : (fun (x : M) => x + a) '' Icc b c = Icc (b + a) (c + a)

@[simp]

theorem Set.image_add_const_Ico {M : Type u_1} [AddCommMonoid M] [PartialOrder M] [IsOrderedCancelAddMonoid M] [ExistsAddOfLE M] (a b c : M) : (fun (x : M) => x + a) '' Ico b c = Ico (b + a) (c + a)

@[simp]

theorem Set.image_add_const_Ioc {M : Type u_1} [AddCommMonoid M] [PartialOrder M] [IsOrderedCancelAddMonoid M] [ExistsAddOfLE M] (a b c : M) : (fun (x : M) => x + a) '' Ioc b c = Ioc (b + a) (c + a)

@[simp]

theorem Set.image_add_const_Ioo {M : Type u_1} [AddCommMonoid M] [PartialOrder M] [IsOrderedCancelAddMonoid M] [ExistsAddOfLE M] (a b c : M) : (fun (x : M) => x + a) '' Ioo b c = Ioo (b + a) (c + a)

Images under x ↦ a + x

@[simp]

theorem Set.image_const_add_Ici {M : Type u_1} [AddCommMonoid M] [PartialOrder M] [IsOrderedCancelAddMonoid M] [ExistsAddOfLE M] (a b : M) : (fun (x : M) => a + x) '' Ici b = Ici (a + b)

@[simp]

theorem Set.image_const_add_Ioi {M : Type u_1} [AddCommMonoid M] [PartialOrder M] [IsOrderedCancelAddMonoid M] [ExistsAddOfLE M] (a b : M) : (fun (x : M) => a + x) '' Ioi b = Ioi (a + b)

@[simp]

theorem Set.image_const_add_Icc {M : Type u_1} [AddCommMonoid M] [PartialOrder M] [IsOrderedCancelAddMonoid M] [ExistsAddOfLE M] (a b c : M) : (fun (x : M) => a + x) '' Icc b c = Icc (a + b) (a + c)

@[simp]

theorem Set.image_const_add_Ico {M : Type u_1} [AddCommMonoid M] [PartialOrder M] [IsOrderedCancelAddMonoid M] [ExistsAddOfLE M] (a b c : M) : (fun (x : M) => a + x) '' Ico b c = Ico (a + b) (a + c)

@[simp]

theorem Set.image_const_add_Ioc {M : Type u_1} [AddCommMonoid M] [PartialOrder M] [IsOrderedCancelAddMonoid M] [ExistsAddOfLE M] (a b c : M) : (fun (x : M) => a + x) '' Ioc b c = Ioc (a + b) (a + c)

@[simp]

theorem Set.image_const_add_Ioo {M : Type u_1} [AddCommMonoid M] [PartialOrder M] [IsOrderedCancelAddMonoid M] [ExistsAddOfLE M] (a b c : M) : (fun (x : M) => a + x) '' Ioo b c = Ioo (a + b) (a + c)