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 OrderedCancelAddCommMonoid; the lemmas below therefore apply to all OrderedAddCommGroup, but also to ℕ and ℝ≥0, which are not groups.

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

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

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

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

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

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

Images under x ↦ x + a

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

Images under x ↦ a + x

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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