mathlib3 documentation

data.set.pointwise.interval

(Pre)images of intervals #

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

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⁻¹.

Preimages under x ↦ a + x #

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

Preimages under x ↦ x + a #

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

Preimages under x ↦ -x #

source
@[simp]
theorem set.preimage_neg_Ici {α : Type u_1} [ordered_add_comm_group α] (a : α) :
-set.Ici a = set.Iic (-a)
source
@[simp]
theorem set.preimage_neg_Iic {α : Type u_1} [ordered_add_comm_group α] (a : α) :
-set.Iic a = set.Ici (-a)
source
@[simp]
theorem set.preimage_neg_Ioi {α : Type u_1} [ordered_add_comm_group α] (a : α) :
-set.Ioi a = set.Iio (-a)
source
@[simp]
theorem set.preimage_neg_Iio {α : Type u_1} [ordered_add_comm_group α] (a : α) :
-set.Iio a = set.Ioi (-a)
source
@[simp]
theorem set.preimage_neg_Icc {α : Type u_1} [ordered_add_comm_group α] (a b : α) :
-set.Icc a b = set.Icc (-b) (-a)
source
@[simp]
theorem set.preimage_neg_Ico {α : Type u_1} [ordered_add_comm_group α] (a b : α) :
-set.Ico a b = set.Ioc (-b) (-a)
source
@[simp]
theorem set.preimage_neg_Ioc {α : Type u_1} [ordered_add_comm_group α] (a b : α) :
-set.Ioc a b = set.Ico (-b) (-a)
source
@[simp]
theorem set.preimage_neg_Ioo {α : Type u_1} [ordered_add_comm_group α] (a b : α) :
-set.Ioo a b = set.Ioo (-b) (-a)

Preimages under x ↦ x - a #

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

Preimages under x ↦ a - x #

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

Images under x ↦ a + x #

source
@[simp]
theorem set.image_const_add_Iic {α : Type u_1} [ordered_add_comm_group α] (a b : α) :
(λ (x : α), a + x) '' set.Iic b = set.Iic (a + b)
source
@[simp]
theorem set.image_const_add_Iio {α : Type u_1} [ordered_add_comm_group α] (a b : α) :
(λ (x : α), a + x) '' set.Iio b = set.Iio (a + b)

Images under x ↦ x + a #

source
@[simp]
theorem set.image_add_const_Iic {α : Type u_1} [ordered_add_comm_group α] (a b : α) :
(λ (x : α), x + a) '' set.Iic b = set.Iic (b + a)
source
@[simp]
theorem set.image_add_const_Iio {α : Type u_1} [ordered_add_comm_group α] (a b : α) :
(λ (x : α), x + a) '' set.Iio b = set.Iio (b + a)

Images under x ↦ -x #

source
theorem set.image_neg_Ici {α : Type u_1} [ordered_add_comm_group α] (a : α) :
has_neg.neg '' set.Ici a = set.Iic (-a)
source
theorem set.image_neg_Iic {α : Type u_1} [ordered_add_comm_group α] (a : α) :
has_neg.neg '' set.Iic a = set.Ici (-a)
source
theorem set.image_neg_Ioi {α : Type u_1} [ordered_add_comm_group α] (a : α) :
has_neg.neg '' set.Ioi a = set.Iio (-a)
source
theorem set.image_neg_Iio {α : Type u_1} [ordered_add_comm_group α] (a : α) :
has_neg.neg '' set.Iio a = set.Ioi (-a)
source
theorem set.image_neg_Icc {α : Type u_1} [ordered_add_comm_group α] (a b : α) :
has_neg.neg '' set.Icc a b = set.Icc (-b) (-a)
source
theorem set.image_neg_Ico {α : Type u_1} [ordered_add_comm_group α] (a b : α) :
has_neg.neg '' set.Ico a b = set.Ioc (-b) (-a)
source
theorem set.image_neg_Ioc {α : Type u_1} [ordered_add_comm_group α] (a b : α) :
has_neg.neg '' set.Ioc a b = set.Ico (-b) (-a)
source
theorem set.image_neg_Ioo {α : Type u_1} [ordered_add_comm_group α] (a b : α) :
has_neg.neg '' set.Ioo a b = set.Ioo (-b) (-a)

Images under x ↦ a - x #

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

Images under x ↦ x - a #

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

Bijections #

source
theorem set.Iic_add_bij {α : Type u_1} [ordered_add_comm_group α] (a b : α) :
set.bij_on (λ (_x : α), _x + a) (set.Iic b) (set.Iic (b + a))
source
theorem set.Iio_add_bij {α : Type u_1} [ordered_add_comm_group α] (a b : α) :
set.bij_on (λ (_x : α), _x + a) (set.Iio b) (set.Iio (b + a))
source
@[simp]
theorem set.preimage_const_add_uIcc {α : Type u_1} [linear_ordered_add_comm_group α] (a b c : α) :
(λ (x : α), a + x) ⁻¹' set.uIcc b c = set.uIcc (b - a) (c - a)
source
@[simp]
theorem set.preimage_add_const_uIcc {α : Type u_1} [linear_ordered_add_comm_group α] (a b c : α) :
(λ (x : α), x + a) ⁻¹' set.uIcc b c = set.uIcc (b - a) (c - a)
source
@[simp]
theorem set.preimage_neg_uIcc {α : Type u_1} [linear_ordered_add_comm_group α] (a b : α) :
-set.uIcc a b = set.uIcc (-a) (-b)
source
@[simp]
theorem set.preimage_sub_const_uIcc {α : Type u_1} [linear_ordered_add_comm_group α] (a b c : α) :
(λ (x : α), x - a) ⁻¹' set.uIcc b c = set.uIcc (b + a) (c + a)
source
@[simp]
theorem set.preimage_const_sub_uIcc {α : Type u_1} [linear_ordered_add_comm_group α] (a b c : α) :
(λ (x : α), a - x) ⁻¹' set.uIcc b c = set.uIcc (a - b) (a - c)
source
@[simp]
theorem set.image_const_add_uIcc {α : Type u_1} [linear_ordered_add_comm_group α] (a b c : α) :
(λ (x : α), a + x) '' set.uIcc b c = set.uIcc (a + b) (a + c)
source
@[simp]
theorem set.image_add_const_uIcc {α : Type u_1} [linear_ordered_add_comm_group α] (a b c : α) :
(λ (x : α), x + a) '' set.uIcc b c = set.uIcc (b + a) (c + a)
source
@[simp]
theorem set.image_const_sub_uIcc {α : Type u_1} [linear_ordered_add_comm_group α] (a b c : α) :
(λ (x : α), a - x) '' set.uIcc b c = set.uIcc (a - b) (a - c)
source
@[simp]
theorem set.image_sub_const_uIcc {α : Type u_1} [linear_ordered_add_comm_group α] (a b c : α) :
(λ (x : α), x - a) '' set.uIcc b c = set.uIcc (b - a) (c - a)
source
theorem set.image_neg_uIcc {α : Type u_1} [linear_ordered_add_comm_group α] (a b : α) :
has_neg.neg '' set.uIcc a b = set.uIcc (-a) (-b)
source
theorem set.abs_sub_le_of_uIcc_subset_uIcc {α : Type u_1} [linear_ordered_add_comm_group α] {a b c d : α} (h : set.uIcc c d ⊆ set.uIcc a b) :
|d - c| ≤ |b - a|

If [c, d] is a subinterval of [a, b], then the distance between c and d is less than or equal to that of a and b

source
theorem set.abs_sub_left_of_mem_uIcc {α : Type u_1} [linear_ordered_add_comm_group α] {a b c : α} (h : c ∈ set.uIcc a b) :
|c - a| ≤ |b - a|

If c ∈ [a, b], then the distance between a and c is less than or equal to that of a and b

source
theorem set.abs_sub_right_of_mem_uIcc {α : Type u_1} [linear_ordered_add_comm_group α] {a b c : α} (h : c ∈ set.uIcc a b) :
|b - c| ≤ |b - a|

If x ∈ [a, b], then the distance between c and b is less than or equal to that of a and b

Multiplication and inverse in a field #

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

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

source
theorem set.inv_Ioi {α : Type u_1} [linear_ordered_field α] {a : α} (ha : 0 < a) :
(set.Ioi a)⁻¹ = set.Ioo 0 a⁻¹
source
theorem set.image_const_mul_Ioi_zero {k : Type u_1} [linear_ordered_field k] {x : k} (hx : 0 < x) :
(λ (y : k), x * y) '' set.Ioi 0 = set.Ioi 0

Images under x ↦ a * x + b #

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