Documentation

Mathlib.Data.Set.Intervals.Monoid

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)