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) :
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) :
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) :
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) :
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) :
@[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) :
@[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) :
@[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) :
@[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) :
@[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) :
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) :
@[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) :
@[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) :
@[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) :
@[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) :
@[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) :