mathlibdocumentation

data.set.intervals.image_preimage

(Pre)images of intervals #

In this file we prove a bunch of trivial lemmas like “if we add a to all points of [b, c], then we get [a + b, a + c]”. For the functions x ↦ x ± a, x ↦ a ± x, and x ↦ -x we prove lemmas about preimages and images of all intervals. We also prove a few lemmas about images under x ↦ a * x, x ↦ x * a and x ↦ x⁻¹.

The lemmas in this section 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.

TODO : move as much as possible in this file to the setting of this weaker typeclass.

theorem set.Icc_add_bij {α : Type u} (a b d : α) :
set.bij_on (λ (_x : α), _x + d) (set.Icc a b) (set.Icc (a + d) (b + d))
theorem set.Ioo_add_bij {α : Type u} (a b d : α) :
set.bij_on (λ (_x : α), _x + d) (set.Ioo a b) (set.Ioo (a + d) (b + d))
theorem set.Ioc_add_bij {α : Type u} (a b d : α) :
set.bij_on (λ (_x : α), _x + d) (set.Ioc a b) (set.Ioc (a + d) (b + d))
theorem set.Ico_add_bij {α : Type u} (a b d : α) :
set.bij_on (λ (_x : α), _x + d) (set.Ico a b) (set.Ico (a + d) (b + d))
theorem set.Ici_add_bij {α : Type u} (a d : α) :
set.bij_on (λ (_x : α), _x + d) (set.Ici a) (set.Ici (a + d))
theorem set.Ioi_add_bij {α : Type u} (a d : α) :
set.bij_on (λ (_x : α), _x + d) (set.Ioi a) (set.Ioi (a + d))

Preimages under x ↦ a + x#

@[simp]
theorem set.preimage_const_add_Ici {G : Type u} (a b : G) :
(λ (x : G), a + x) ⁻¹' = set.Ici (b - a)
@[simp]
theorem set.preimage_const_add_Ioi {G : Type u} (a b : G) :
(λ (x : G), a + x) ⁻¹' = set.Ioi (b - a)
@[simp]
theorem set.preimage_const_add_Iic {G : Type u} (a b : G) :
(λ (x : G), a + x) ⁻¹' = set.Iic (b - a)
@[simp]
theorem set.preimage_const_add_Iio {G : Type u} (a b : G) :
(λ (x : G), a + x) ⁻¹' = set.Iio (b - a)
@[simp]
theorem set.preimage_const_add_Icc {G : Type u} (a b c : G) :
(λ (x : G), a + x) ⁻¹' c = set.Icc (b - a) (c - a)
@[simp]
theorem set.preimage_const_add_Ico {G : Type u} (a b c : G) :
(λ (x : G), a + x) ⁻¹' c = set.Ico (b - a) (c - a)
@[simp]
theorem set.preimage_const_add_Ioc {G : Type u} (a b c : G) :
(λ (x : G), a + x) ⁻¹' c = set.Ioc (b - a) (c - a)
@[simp]
theorem set.preimage_const_add_Ioo {G : Type u} (a b c : G) :
(λ (x : G), a + x) ⁻¹' c = set.Ioo (b - a) (c - a)

Preimages under x ↦ x + a#

@[simp]
theorem set.preimage_add_const_Ici {G : Type u} (a b : G) :
(λ (x : G), x + a) ⁻¹' = set.Ici (b - a)
@[simp]
theorem set.preimage_add_const_Ioi {G : Type u} (a b : G) :
(λ (x : G), x + a) ⁻¹' = set.Ioi (b - a)
@[simp]
theorem set.preimage_add_const_Iic {G : Type u} (a b : G) :
(λ (x : G), x + a) ⁻¹' = set.Iic (b - a)
@[simp]
theorem set.preimage_add_const_Iio {G : Type u} (a b : G) :
(λ (x : G), x + a) ⁻¹' = set.Iio (b - a)
@[simp]
theorem set.preimage_add_const_Icc {G : Type u} (a b c : G) :
(λ (x : G), x + a) ⁻¹' c = set.Icc (b - a) (c - a)
@[simp]
theorem set.preimage_add_const_Ico {G : Type u} (a b c : G) :
(λ (x : G), x + a) ⁻¹' c = set.Ico (b - a) (c - a)
@[simp]
theorem set.preimage_add_const_Ioc {G : Type u} (a b c : G) :
(λ (x : G), x + a) ⁻¹' c = set.Ioc (b - a) (c - a)
@[simp]
theorem set.preimage_add_const_Ioo {G : Type u} (a b c : G) :
(λ (x : G), x + a) ⁻¹' c = set.Ioo (b - a) (c - a)

Preimages under x ↦ -x#

@[simp]
theorem set.preimage_neg_Ici {G : Type u} (a : G) :
@[simp]
theorem set.preimage_neg_Iic {G : Type u} (a : G) :
@[simp]
theorem set.preimage_neg_Ioi {G : Type u} (a : G) :
@[simp]
theorem set.preimage_neg_Iio {G : Type u} (a : G) :
@[simp]
theorem set.preimage_neg_Icc {G : Type u} (a b : G) :
- b = set.Icc (-b) (-a)
@[simp]
theorem set.preimage_neg_Ico {G : Type u} (a b : G) :
- b = set.Ioc (-b) (-a)
@[simp]
theorem set.preimage_neg_Ioc {G : Type u} (a b : G) :
- b = set.Ico (-b) (-a)
@[simp]
theorem set.preimage_neg_Ioo {G : Type u} (a b : G) :
- b = set.Ioo (-b) (-a)

Preimages under x ↦ x - a#

@[simp]
theorem set.preimage_sub_const_Ici {G : Type u} (a b : G) :
(λ (x : G), x - a) ⁻¹' = set.Ici (b + a)
@[simp]
theorem set.preimage_sub_const_Ioi {G : Type u} (a b : G) :
(λ (x : G), x - a) ⁻¹' = set.Ioi (b + a)
@[simp]
theorem set.preimage_sub_const_Iic {G : Type u} (a b : G) :
(λ (x : G), x - a) ⁻¹' = set.Iic (b + a)
@[simp]
theorem set.preimage_sub_const_Iio {G : Type u} (a b : G) :
(λ (x : G), x - a) ⁻¹' = set.Iio (b + a)
@[simp]
theorem set.preimage_sub_const_Icc {G : Type u} (a b c : G) :
(λ (x : G), x - a) ⁻¹' c = set.Icc (b + a) (c + a)
@[simp]
theorem set.preimage_sub_const_Ico {G : Type u} (a b c : G) :
(λ (x : G), x - a) ⁻¹' c = set.Ico (b + a) (c + a)
@[simp]
theorem set.preimage_sub_const_Ioc {G : Type u} (a b c : G) :
(λ (x : G), x - a) ⁻¹' c = set.Ioc (b + a) (c + a)
@[simp]
theorem set.preimage_sub_const_Ioo {G : Type u} (a b c : G) :
(λ (x : G), x - a) ⁻¹' c = set.Ioo (b + a) (c + a)

Preimages under x ↦ a - x#

@[simp]
theorem set.preimage_const_sub_Ici {G : Type u} (a b : G) :
(λ (x : G), a - x) ⁻¹' = set.Iic (a - b)
@[simp]
theorem set.preimage_const_sub_Iic {G : Type u} (a b : G) :
(λ (x : G), a - x) ⁻¹' = set.Ici (a - b)
@[simp]
theorem set.preimage_const_sub_Ioi {G : Type u} (a b : G) :
(λ (x : G), a - x) ⁻¹' = set.Iio (a - b)
@[simp]
theorem set.preimage_const_sub_Iio {G : Type u} (a b : G) :
(λ (x : G), a - x) ⁻¹' = set.Ioi (a - b)
@[simp]
theorem set.preimage_const_sub_Icc {G : Type u} (a b c : G) :
(λ (x : G), a - x) ⁻¹' c = set.Icc (a - c) (a - b)
@[simp]
theorem set.preimage_const_sub_Ico {G : Type u} (a b c : G) :
(λ (x : G), a - x) ⁻¹' c = set.Ioc (a - c) (a - b)
@[simp]
theorem set.preimage_const_sub_Ioc {G : Type u} (a b c : G) :
(λ (x : G), a - x) ⁻¹' c = set.Ico (a - c) (a - b)
@[simp]
theorem set.preimage_const_sub_Ioo {G : Type u} (a b c : G) :
(λ (x : G), a - x) ⁻¹' c = set.Ioo (a - c) (a - b)

Images under x ↦ a + x#

@[simp]
theorem set.image_const_add_Ici {G : Type u} (a b : G) :
(λ (x : G), a + x) '' = set.Ici (a + b)
@[simp]
theorem set.image_const_add_Iic {G : Type u} (a b : G) :
(λ (x : G), a + x) '' = set.Iic (a + b)
@[simp]
theorem set.image_const_add_Iio {G : Type u} (a b : G) :
(λ (x : G), a + x) '' = set.Iio (a + b)
@[simp]
theorem set.image_const_add_Ioi {G : Type u} (a b : G) :
(λ (x : G), a + x) '' = set.Ioi (a + b)
@[simp]
theorem set.image_const_add_Icc {G : Type u} (a b c : G) :
(λ (x : G), a + x) '' c = set.Icc (a + b) (a + c)
@[simp]
theorem set.image_const_add_Ico {G : Type u} (a b c : G) :
(λ (x : G), a + x) '' c = set.Ico (a + b) (a + c)
@[simp]
theorem set.image_const_add_Ioc {G : Type u} (a b c : G) :
(λ (x : G), a + x) '' c = set.Ioc (a + b) (a + c)
@[simp]
theorem set.image_const_add_Ioo {G : Type u} (a b c : G) :
(λ (x : G), a + x) '' c = set.Ioo (a + b) (a + c)

Images under x ↦ x + a#

@[simp]
theorem set.image_add_const_Ici {G : Type u} (a b : G) :
(λ (x : G), x + a) '' = set.Ici (b + a)
@[simp]
theorem set.image_add_const_Iic {G : Type u} (a b : G) :
(λ (x : G), x + a) '' = set.Iic (b + a)
@[simp]
theorem set.image_add_const_Iio {G : Type u} (a b : G) :
(λ (x : G), x + a) '' = set.Iio (b + a)
@[simp]
theorem set.image_add_const_Ioi {G : Type u} (a b : G) :
(λ (x : G), x + a) '' = set.Ioi (b + a)
@[simp]
theorem set.image_add_const_Icc {G : Type u} (a b c : G) :
(λ (x : G), x + a) '' c = set.Icc (b + a) (c + a)
@[simp]
theorem set.image_add_const_Ico {G : Type u} (a b c : G) :
(λ (x : G), x + a) '' c = set.Ico (b + a) (c + a)
@[simp]
theorem set.image_add_const_Ioc {G : Type u} (a b c : G) :
(λ (x : G), x + a) '' c = set.Ioc (b + a) (c + a)
@[simp]
theorem set.image_add_const_Ioo {G : Type u} (a b c : G) :
(λ (x : G), x + a) '' c = set.Ioo (b + a) (c + a)

Images under x ↦ -x#

theorem set.image_neg_Ici {G : Type u} (a : G) :
= set.Iic (-a)
theorem set.image_neg_Iic {G : Type u} (a : G) :
= set.Ici (-a)
theorem set.image_neg_Ioi {G : Type u} (a : G) :
= set.Iio (-a)
theorem set.image_neg_Iio {G : Type u} (a : G) :
= set.Ioi (-a)
theorem set.image_neg_Icc {G : Type u} (a b : G) :
= set.Icc (-b) (-a)
theorem set.image_neg_Ico {G : Type u} (a b : G) :
= set.Ioc (-b) (-a)
theorem set.image_neg_Ioc {G : Type u} (a b : G) :
= set.Ico (-b) (-a)
theorem set.image_neg_Ioo {G : Type u} (a b : G) :
= set.Ioo (-b) (-a)

Images under x ↦ a - x#

@[simp]
theorem set.image_const_sub_Ici {G : Type u} (a b : G) :
(λ (x : G), a - x) '' = set.Iic (a - b)
@[simp]
theorem set.image_const_sub_Iic {G : Type u} (a b : G) :
(λ (x : G), a - x) '' = set.Ici (a - b)
@[simp]
theorem set.image_const_sub_Ioi {G : Type u} (a b : G) :
(λ (x : G), a - x) '' = set.Iio (a - b)
@[simp]
theorem set.image_const_sub_Iio {G : Type u} (a b : G) :
(λ (x : G), a - x) '' = set.Ioi (a - b)
@[simp]
theorem set.image_const_sub_Icc {G : Type u} (a b c : G) :
(λ (x : G), a - x) '' c = set.Icc (a - c) (a - b)
@[simp]
theorem set.image_const_sub_Ico {G : Type u} (a b c : G) :
(λ (x : G), a - x) '' c = set.Ioc (a - c) (a - b)
@[simp]
theorem set.image_const_sub_Ioc {G : Type u} (a b c : G) :
(λ (x : G), a - x) '' c = set.Ico (a - c) (a - b)
@[simp]
theorem set.image_const_sub_Ioo {G : Type u} (a b c : G) :
(λ (x : G), a - x) '' c = set.Ioo (a - c) (a - b)

Images under x ↦ x - a#

@[simp]
theorem set.image_sub_const_Ici {G : Type u} (a b : G) :
(λ (x : G), x - a) '' = set.Ici (b - a)
@[simp]
theorem set.image_sub_const_Iic {G : Type u} (a b : G) :
(λ (x : G), x - a) '' = set.Iic (b - a)
@[simp]
theorem set.image_sub_const_Ioi {G : Type u} (a b : G) :
(λ (x : G), x - a) '' = set.Ioi (b - a)
@[simp]
theorem set.image_sub_const_Iio {G : Type u} (a b : G) :
(λ (x : G), x - a) '' = set.Iio (b - a)
@[simp]
theorem set.image_sub_const_Icc {G : Type u} (a b c : G) :
(λ (x : G), x - a) '' c = set.Icc (b - a) (c - a)
@[simp]
theorem set.image_sub_const_Ico {G : Type u} (a b c : G) :
(λ (x : G), x - a) '' c = set.Ico (b - a) (c - a)
@[simp]
theorem set.image_sub_const_Ioc {G : Type u} (a b c : G) :
(λ (x : G), x - a) '' c = set.Ioc (b - a) (c - a)
@[simp]
theorem set.image_sub_const_Ioo {G : Type u} (a b c : G) :
(λ (x : G), x - a) '' c = set.Ioo (b - a) (c - a)

Bijections #

theorem set.Iic_add_bij {G : Type u} (a b : G) :
set.bij_on (λ (_x : G), _x + a) (set.Iic b) (set.Iic (b + a))
theorem set.Iio_add_bij {G : Type u} (a b : G) :
set.bij_on (λ (_x : G), _x + a) (set.Iio b) (set.Iio (b + a))

Multiplication and inverse in a field #

@[simp]
theorem set.preimage_mul_const_Iio {k : Type u} (a : k) {c : k} (h : 0 < c) :
(λ (x : k), x * c) ⁻¹' = set.Iio (a / c)
@[simp]
theorem set.preimage_mul_const_Ioi {k : Type u} (a : k) {c : k} (h : 0 < c) :
(λ (x : k), x * c) ⁻¹' = set.Ioi (a / c)
@[simp]
theorem set.preimage_mul_const_Iic {k : Type u} (a : k) {c : k} (h : 0 < c) :
(λ (x : k), x * c) ⁻¹' = set.Iic (a / c)
@[simp]
theorem set.preimage_mul_const_Ici {k : Type u} (a : k) {c : k} (h : 0 < c) :
(λ (x : k), x * c) ⁻¹' = set.Ici (a / c)
@[simp]
theorem set.preimage_mul_const_Ioo {k : Type u} (a b : k) {c : k} (h : 0 < c) :
(λ (x : k), x * c) ⁻¹' b = set.Ioo (a / c) (b / c)
@[simp]
theorem set.preimage_mul_const_Ioc {k : Type u} (a b : k) {c : k} (h : 0 < c) :
(λ (x : k), x * c) ⁻¹' b = set.Ioc (a / c) (b / c)
@[simp]
theorem set.preimage_mul_const_Ico {k : Type u} (a b : k) {c : k} (h : 0 < c) :
(λ (x : k), x * c) ⁻¹' b = set.Ico (a / c) (b / c)
@[simp]
theorem set.preimage_mul_const_Icc {k : Type u} (a b : k) {c : k} (h : 0 < c) :
(λ (x : k), x * c) ⁻¹' b = set.Icc (a / c) (b / c)
@[simp]
theorem set.preimage_mul_const_Iio_of_neg {k : Type u} (a : k) {c : k} (h : c < 0) :
(λ (x : k), x * c) ⁻¹' = set.Ioi (a / c)
@[simp]
theorem set.preimage_mul_const_Ioi_of_neg {k : Type u} (a : k) {c : k} (h : c < 0) :
(λ (x : k), x * c) ⁻¹' = set.Iio (a / c)
@[simp]
theorem set.preimage_mul_const_Iic_of_neg {k : Type u} (a : k) {c : k} (h : c < 0) :
(λ (x : k), x * c) ⁻¹' = set.Ici (a / c)
@[simp]
theorem set.preimage_mul_const_Ici_of_neg {k : Type u} (a : k) {c : k} (h : c < 0) :
(λ (x : k), x * c) ⁻¹' = set.Iic (a / c)
@[simp]
theorem set.preimage_mul_const_Ioo_of_neg {k : Type u} (a b : k) {c : k} (h : c < 0) :
(λ (x : k), x * c) ⁻¹' b = set.Ioo (b / c) (a / c)
@[simp]
theorem set.preimage_mul_const_Ioc_of_neg {k : Type u} (a b : k) {c : k} (h : c < 0) :
(λ (x : k), x * c) ⁻¹' b = set.Ico (b / c) (a / c)
@[simp]
theorem set.preimage_mul_const_Ico_of_neg {k : Type u} (a b : k) {c : k} (h : c < 0) :
(λ (x : k), x * c) ⁻¹' b = set.Ioc (b / c) (a / c)
@[simp]
theorem set.preimage_mul_const_Icc_of_neg {k : Type u} (a b : k) {c : k} (h : c < 0) :
(λ (x : k), x * c) ⁻¹' b = set.Icc (b / c) (a / c)
@[simp]
theorem set.preimage_const_mul_Iio {k : Type u} (a : k) {c : k} (h : 0 < c) :
= set.Iio (a / c)
@[simp]
theorem set.preimage_const_mul_Ioi {k : Type u} (a : k) {c : k} (h : 0 < c) :
= set.Ioi (a / c)
@[simp]
theorem set.preimage_const_mul_Iic {k : Type u} (a : k) {c : k} (h : 0 < c) :
= set.Iic (a / c)
@[simp]
theorem set.preimage_const_mul_Ici {k : Type u} (a : k) {c : k} (h : 0 < c) :
= set.Ici (a / c)
@[simp]
theorem set.preimage_const_mul_Ioo {k : Type u} (a b : k) {c : k} (h : 0 < c) :
⁻¹' b = set.Ioo (a / c) (b / c)
@[simp]
theorem set.preimage_const_mul_Ioc {k : Type u} (a b : k) {c : k} (h : 0 < c) :
⁻¹' b = set.Ioc (a / c) (b / c)
@[simp]
theorem set.preimage_const_mul_Ico {k : Type u} (a b : k) {c : k} (h : 0 < c) :
⁻¹' b = set.Ico (a / c) (b / c)
@[simp]
theorem set.preimage_const_mul_Icc {k : Type u} (a b : k) {c : k} (h : 0 < c) :
⁻¹' b = set.Icc (a / c) (b / c)
@[simp]
theorem set.preimage_const_mul_Iio_of_neg {k : Type u} (a : k) {c : k} (h : c < 0) :
= set.Ioi (a / c)
@[simp]
theorem set.preimage_const_mul_Ioi_of_neg {k : Type u} (a : k) {c : k} (h : c < 0) :
= set.Iio (a / c)
@[simp]
theorem set.preimage_const_mul_Iic_of_neg {k : Type u} (a : k) {c : k} (h : c < 0) :
= set.Ici (a / c)
@[simp]
theorem set.preimage_const_mul_Ici_of_neg {k : Type u} (a : k) {c : k} (h : c < 0) :
= set.Iic (a / c)
@[simp]
theorem set.preimage_const_mul_Ioo_of_neg {k : Type u} (a b : k) {c : k} (h : c < 0) :
⁻¹' b = set.Ioo (b / c) (a / c)
@[simp]
theorem set.preimage_const_mul_Ioc_of_neg {k : Type u} (a b : k) {c : k} (h : c < 0) :
⁻¹' b = set.Ico (b / c) (a / c)
@[simp]
theorem set.preimage_const_mul_Ico_of_neg {k : Type u} (a b : k) {c : k} (h : c < 0) :
⁻¹' b = set.Ioc (b / c) (a / c)
@[simp]
theorem set.preimage_const_mul_Icc_of_neg {k : Type u} (a b : k) {c : k} (h : c < 0) :
⁻¹' b = set.Icc (b / c) (a / c)
theorem set.image_mul_right_Icc' {k : Type u} (a b : k) {c : k} (h : 0 < c) :
(λ (x : k), x * c) '' b = set.Icc (a * c) (b * c)
theorem set.image_mul_right_Icc {k : Type u} {a b c : k} (hab : a b) (hc : 0 c) :
(λ (x : k), x * c) '' b = set.Icc (a * c) (b * c)
theorem set.image_mul_left_Icc' {k : Type u} {a : k} (h : 0 < a) (b c : k) :
'' c = set.Icc (a * b) (a * c)
theorem set.image_mul_left_Icc {k : Type u} {a b c : k} (ha : 0 a) (hbc : b c) :
'' c = set.Icc (a * b) (a * c)
theorem set.image_mul_right_Ioo {k : Type u} (a b : k) {c : k} (h : 0 < c) :
(λ (x : k), x * c) '' b = set.Ioo (a * c) (b * c)
theorem set.image_mul_left_Ioo {k : Type u} {a : k} (h : 0 < a) (b c : k) :
'' c = set.Ioo (a * b) (a * c)
theorem set.inv_Ioo_0_left {k : Type u} {a : k} (ha : 0 < a) :

The (pre)image under inv of Ioo 0 a is Ioi a⁻¹.

theorem set.inv_Ioi {k : Type u} {a : k} (ha : 0 < a) :

Images under x ↦ a * x + b#

@[simp]
theorem set.image_affine_Icc' {k : Type u} {a : k} (h : 0 < a) (b c d : k) :
(λ (x : k), a * x + b) '' d = set.Icc (a * c + b) (a * d + b)