mathlib3 documentation

data.set.intervals.monoid

Images of intervals under (+ d) #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

theorem set.Ici_add_bij {M : Type u_1} [ordered_cancel_add_comm_monoid M] [has_exists_add_of_le M] (a d : M) :
set.bij_on (λ (_x : M), _x + d) (set.Ici a) (set.Ici (a + d))
theorem set.Ioi_add_bij {M : Type u_1} [ordered_cancel_add_comm_monoid M] [has_exists_add_of_le M] (a d : M) :
set.bij_on (λ (_x : M), _x + d) (set.Ioi a) (set.Ioi (a + d))
theorem set.Icc_add_bij {M : Type u_1} [ordered_cancel_add_comm_monoid M] [has_exists_add_of_le M] (a b d : M) :
set.bij_on (λ (_x : M), _x + d) (set.Icc a b) (set.Icc (a + d) (b + d))
theorem set.Ioo_add_bij {M : Type u_1} [ordered_cancel_add_comm_monoid M] [has_exists_add_of_le M] (a b d : M) :
set.bij_on (λ (_x : M), _x + d) (set.Ioo a b) (set.Ioo (a + d) (b + d))
theorem set.Ioc_add_bij {M : Type u_1} [ordered_cancel_add_comm_monoid M] [has_exists_add_of_le M] (a b d : M) :
set.bij_on (λ (_x : M), _x + d) (set.Ioc a b) (set.Ioc (a + d) (b + d))
theorem set.Ico_add_bij {M : Type u_1} [ordered_cancel_add_comm_monoid M] [has_exists_add_of_le M] (a b d : M) :
set.bij_on (λ (_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} [ordered_cancel_add_comm_monoid M] [has_exists_add_of_le M] (a b : M) :
(λ (x : M), x + a) '' set.Ici b = set.Ici (b + a)
@[simp]
theorem set.image_add_const_Ioi {M : Type u_1} [ordered_cancel_add_comm_monoid M] [has_exists_add_of_le M] (a b : M) :
(λ (x : M), x + a) '' set.Ioi b = set.Ioi (b + a)
@[simp]
theorem set.image_add_const_Icc {M : Type u_1} [ordered_cancel_add_comm_monoid M] [has_exists_add_of_le M] (a b c : M) :
(λ (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} [ordered_cancel_add_comm_monoid M] [has_exists_add_of_le M] (a b c : M) :
(λ (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} [ordered_cancel_add_comm_monoid M] [has_exists_add_of_le M] (a b c : M) :
(λ (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} [ordered_cancel_add_comm_monoid M] [has_exists_add_of_le M] (a b c : M) :
(λ (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} [ordered_cancel_add_comm_monoid M] [has_exists_add_of_le M] (a b : M) :
(λ (x : M), a + x) '' set.Ici b = set.Ici (a + b)
@[simp]
theorem set.image_const_add_Ioi {M : Type u_1} [ordered_cancel_add_comm_monoid M] [has_exists_add_of_le M] (a b : M) :
(λ (x : M), a + x) '' set.Ioi b = set.Ioi (a + b)
@[simp]
theorem set.image_const_add_Icc {M : Type u_1} [ordered_cancel_add_comm_monoid M] [has_exists_add_of_le M] (a b c : M) :
(λ (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} [ordered_cancel_add_comm_monoid M] [has_exists_add_of_le M] (a b c : M) :
(λ (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} [ordered_cancel_add_comm_monoid M] [has_exists_add_of_le M] (a b c : M) :
(λ (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} [ordered_cancel_add_comm_monoid M] [has_exists_add_of_le M] (a b c : M) :
(λ (x : M), a + x) '' set.Ioo b c = set.Ioo (a + b) (a + c)