mathlib docs: data.set.intervals.image

source

@[simp]

theorem set.preimage_const_add_Ici {G : Type u} [ordered_add_comm_group G] (a b : G) :

(λ (x : G), a + x) ⁻¹' set.Ici b = set.Ici (b - a)

source

@[simp]

theorem set.preimage_const_add_Ioi {G : Type u} [ordered_add_comm_group G] (a b : G) :

(λ (x : G), a + x) ⁻¹' set.Ioi b = set.Ioi (b - a)

source

@[simp]

theorem set.preimage_const_add_Iic {G : Type u} [ordered_add_comm_group G] (a b : G) :

(λ (x : G), a + x) ⁻¹' set.Iic b = set.Iic (b - a)

source

@[simp]

theorem set.preimage_const_add_Iio {G : Type u} [ordered_add_comm_group G] (a b : G) :

(λ (x : G), a + x) ⁻¹' set.Iio b = set.Iio (b - a)

source

@[simp]

theorem set.preimage_const_add_Icc {G : Type u} [ordered_add_comm_group G] (a b c : G) :

(λ (x : G), a + x) ⁻¹' set.Icc b c = set.Icc (b - a) (c - a)

source

@[simp]

theorem set.preimage_const_add_Ico {G : Type u} [ordered_add_comm_group G] (a b c : G) :

(λ (x : G), a + x) ⁻¹' set.Ico b c = set.Ico (b - a) (c - a)

source

@[simp]

theorem set.preimage_const_add_Ioc {G : Type u} [ordered_add_comm_group G] (a b c : G) :

(λ (x : G), a + x) ⁻¹' set.Ioc b c = set.Ioc (b - a) (c - a)

source

@[simp]

theorem set.preimage_const_add_Ioo {G : Type u} [ordered_add_comm_group G] (a b c : G) :

(λ (x : G), a + x) ⁻¹' set.Ioo b c = set.Ioo (b - a) (c - a)

source

@[simp]

theorem set.preimage_add_const_Ici {G : Type u} [ordered_add_comm_group G] (a b : G) :

(λ (x : G), x + a) ⁻¹' set.Ici b = set.Ici (b - a)

source

@[simp]

theorem set.preimage_add_const_Ioi {G : Type u} [ordered_add_comm_group G] (a b : G) :

(λ (x : G), x + a) ⁻¹' set.Ioi b = set.Ioi (b - a)

source

@[simp]

theorem set.preimage_add_const_Iic {G : Type u} [ordered_add_comm_group G] (a b : G) :

(λ (x : G), x + a) ⁻¹' set.Iic b = set.Iic (b - a)

source

@[simp]

theorem set.preimage_add_const_Iio {G : Type u} [ordered_add_comm_group G] (a b : G) :

(λ (x : G), x + a) ⁻¹' set.Iio b = set.Iio (b - a)

source

@[simp]

theorem set.preimage_add_const_Icc {G : Type u} [ordered_add_comm_group G] (a b c : G) :

(λ (x : G), x + a) ⁻¹' set.Icc b c = set.Icc (b - a) (c - a)

source

@[simp]

theorem set.preimage_add_const_Ico {G : Type u} [ordered_add_comm_group G] (a b c : G) :

(λ (x : G), x + a) ⁻¹' set.Ico b c = set.Ico (b - a) (c - a)

source

@[simp]

theorem set.preimage_add_const_Ioc {G : Type u} [ordered_add_comm_group G] (a b c : G) :

(λ (x : G), x + a) ⁻¹' set.Ioc b c = set.Ioc (b - a) (c - a)

source

@[simp]

theorem set.preimage_add_const_Ioo {G : Type u} [ordered_add_comm_group G] (a b c : G) :

(λ (x : G), x + a) ⁻¹' set.Ioo b c = set.Ioo (b - a) (c - a)

source

@[simp]

theorem set.preimage_neg_Ici {G : Type u} [ordered_add_comm_group G] (a : G) :

-set.Ici a = set.Iic (-a)

source

@[simp]

theorem set.preimage_neg_Iic {G : Type u} [ordered_add_comm_group G] (a : G) :

-set.Iic a = set.Ici (-a)

source

@[simp]

theorem set.preimage_neg_Ioi {G : Type u} [ordered_add_comm_group G] (a : G) :

-set.Ioi a = set.Iio (-a)

source

@[simp]

theorem set.preimage_neg_Iio {G : Type u} [ordered_add_comm_group G] (a : G) :

-set.Iio a = set.Ioi (-a)

source

@[simp]

theorem set.preimage_neg_Icc {G : Type u} [ordered_add_comm_group G] (a b : G) :

-set.Icc a b = set.Icc (-b) (-a)

source

@[simp]

theorem set.preimage_neg_Ico {G : Type u} [ordered_add_comm_group G] (a b : G) :

-set.Ico a b = set.Ioc (-b) (-a)

source

@[simp]

theorem set.preimage_neg_Ioc {G : Type u} [ordered_add_comm_group G] (a b : G) :

-set.Ioc a b = set.Ico (-b) (-a)

source

@[simp]

theorem set.preimage_neg_Ioo {G : Type u} [ordered_add_comm_group G] (a b : G) :

-set.Ioo a b = set.Ioo (-b) (-a)

source

@[simp]

theorem set.preimage_sub_const_Ici {G : Type u} [ordered_add_comm_group G] (a b : G) :

(λ (x : G), x - a) ⁻¹' set.Ici b = set.Ici (b + a)

source

@[simp]

theorem set.preimage_sub_const_Ioi {G : Type u} [ordered_add_comm_group G] (a b : G) :

(λ (x : G), x - a) ⁻¹' set.Ioi b = set.Ioi (b + a)

source

@[simp]

theorem set.preimage_sub_const_Iic {G : Type u} [ordered_add_comm_group G] (a b : G) :

(λ (x : G), x - a) ⁻¹' set.Iic b = set.Iic (b + a)

source

@[simp]

theorem set.preimage_sub_const_Iio {G : Type u} [ordered_add_comm_group G] (a b : G) :

(λ (x : G), x - a) ⁻¹' set.Iio b = set.Iio (b + a)

source

@[simp]

theorem set.preimage_sub_const_Icc {G : Type u} [ordered_add_comm_group G] (a b c : G) :

(λ (x : G), x - a) ⁻¹' set.Icc b c = set.Icc (b + a) (c + a)

source

@[simp]

theorem set.preimage_sub_const_Ico {G : Type u} [ordered_add_comm_group G] (a b c : G) :

(λ (x : G), x - a) ⁻¹' set.Ico b c = set.Ico (b + a) (c + a)

source

@[simp]

theorem set.preimage_sub_const_Ioc {G : Type u} [ordered_add_comm_group G] (a b c : G) :

(λ (x : G), x - a) ⁻¹' set.Ioc b c = set.Ioc (b + a) (c + a)

source

@[simp]

theorem set.preimage_sub_const_Ioo {G : Type u} [ordered_add_comm_group G] (a b c : G) :

(λ (x : G), x - a) ⁻¹' set.Ioo b c = set.Ioo (b + a) (c + a)

source

@[simp]

theorem set.preimage_const_sub_Ici {G : Type u} [ordered_add_comm_group G] (a b : G) :

(λ (x : G), a - x) ⁻¹' set.Ici b = set.Iic (a - b)

source

@[simp]

theorem set.preimage_const_sub_Iic {G : Type u} [ordered_add_comm_group G] (a b : G) :

(λ (x : G), a - x) ⁻¹' set.Iic b = set.Ici (a - b)

source

@[simp]

theorem set.preimage_const_sub_Ioi {G : Type u} [ordered_add_comm_group G] (a b : G) :

(λ (x : G), a - x) ⁻¹' set.Ioi b = set.Iio (a - b)

source

@[simp]

theorem set.preimage_const_sub_Iio {G : Type u} [ordered_add_comm_group G] (a b : G) :

(λ (x : G), a - x) ⁻¹' set.Iio b = set.Ioi (a - b)

source

@[simp]

theorem set.preimage_const_sub_Icc {G : Type u} [ordered_add_comm_group G] (a b c : G) :

(λ (x : G), a - x) ⁻¹' set.Icc b c = set.Icc (a - c) (a - b)

source

@[simp]

theorem set.preimage_const_sub_Ico {G : Type u} [ordered_add_comm_group G] (a b c : G) :

(λ (x : G), a - x) ⁻¹' set.Ico b c = set.Ioc (a - c) (a - b)

source

@[simp]

theorem set.preimage_const_sub_Ioc {G : Type u} [ordered_add_comm_group G] (a b c : G) :

(λ (x : G), a - x) ⁻¹' set.Ioc b c = set.Ico (a - c) (a - b)

source

@[simp]

theorem set.preimage_const_sub_Ioo {G : Type u} [ordered_add_comm_group G] (a b c : G) :

(λ (x : G), a - x) ⁻¹' set.Ioo b c = set.Ioo (a - c) (a - b)

source

@[simp]

theorem set.image_const_add_Ici {G : Type u} [ordered_add_comm_group G] (a b : G) :

(λ (x : G), a + x) '' set.Ici b = set.Ici (a + b)

source

@[simp]

theorem set.image_const_add_Iic {G : Type u} [ordered_add_comm_group G] (a b : G) :

(λ (x : G), a + x) '' set.Iic b = set.Iic (a + b)

source

@[simp]

theorem set.image_const_add_Iio {G : Type u} [ordered_add_comm_group G] (a b : G) :

(λ (x : G), a + x) '' set.Iio b = set.Iio (a + b)

source

@[simp]

theorem set.image_const_add_Ioi {G : Type u} [ordered_add_comm_group G] (a b : G) :

(λ (x : G), a + x) '' set.Ioi b = set.Ioi (a + b)

source

@[simp]

theorem set.image_const_add_Icc {G : Type u} [ordered_add_comm_group G] (a b c : G) :

(λ (x : G), a + x) '' set.Icc b c = set.Icc (a + b) (a + c)

source

@[simp]

theorem set.image_const_add_Ico {G : Type u} [ordered_add_comm_group G] (a b c : G) :

(λ (x : G), a + x) '' set.Ico b c = set.Ico (a + b) (a + c)

source

@[simp]

theorem set.image_const_add_Ioc {G : Type u} [ordered_add_comm_group G] (a b c : G) :

(λ (x : G), a + x) '' set.Ioc b c = set.Ioc (a + b) (a + c)

source

@[simp]

theorem set.image_const_add_Ioo {G : Type u} [ordered_add_comm_group G] (a b c : G) :

(λ (x : G), a + x) '' set.Ioo b c = set.Ioo (a + b) (a + c)

source

@[simp]

theorem set.image_add_const_Ici {G : Type u} [ordered_add_comm_group G] (a b : G) :

(λ (x : G), x + a) '' set.Ici b = set.Ici (a + b)

source

@[simp]

theorem set.image_add_const_Iic {G : Type u} [ordered_add_comm_group G] (a b : G) :

(λ (x : G), x + a) '' set.Iic b = set.Iic (a + b)

source

@[simp]

theorem set.image_add_const_Iio {G : Type u} [ordered_add_comm_group G] (a b : G) :

(λ (x : G), x + a) '' set.Iio b = set.Iio (a + b)

source

@[simp]

theorem set.image_add_const_Ioi {G : Type u} [ordered_add_comm_group G] (a b : G) :

(λ (x : G), x + a) '' set.Ioi b = set.Ioi (a + b)

source

@[simp]

theorem set.image_add_const_Icc {G : Type u} [ordered_add_comm_group G] (a b c : G) :

(λ (x : G), x + a) '' set.Icc b c = set.Icc (a + b) (a + c)

source

@[simp]

theorem set.image_add_const_Ico {G : Type u} [ordered_add_comm_group G] (a b c : G) :

(λ (x : G), x + a) '' set.Ico b c = set.Ico (a + b) (a + c)

source

@[simp]

theorem set.image_add_const_Ioc {G : Type u} [ordered_add_comm_group G] (a b c : G) :

(λ (x : G), x + a) '' set.Ioc b c = set.Ioc (a + b) (a + c)

source

@[simp]

theorem set.image_add_const_Ioo {G : Type u} [ordered_add_comm_group G] (a b c : G) :

(λ (x : G), x + a) '' set.Ioo b c = set.Ioo (a + b) (a + c)

source

theorem set.image_neg_Ici {G : Type u} [ordered_add_comm_group G] (a : G) :

has_neg.neg '' set.Ici a = set.Iic (-a)

source

theorem set.image_neg_Iic {G : Type u} [ordered_add_comm_group G] (a : G) :

has_neg.neg '' set.Iic a = set.Ici (-a)

source

theorem set.image_neg_Ioi {G : Type u} [ordered_add_comm_group G] (a : G) :

has_neg.neg '' set.Ioi a = set.Iio (-a)

source

theorem set.image_neg_Iio {G : Type u} [ordered_add_comm_group G] (a : G) :

has_neg.neg '' set.Iio a = set.Ioi (-a)

source

theorem set.image_neg_Icc {G : Type u} [ordered_add_comm_group G] (a b : G) :

has_neg.neg '' set.Icc a b = set.Icc (-b) (-a)

source

theorem set.image_neg_Ico {G : Type u} [ordered_add_comm_group G] (a b : G) :

has_neg.neg '' set.Ico a b = set.Ioc (-b) (-a)

source

theorem set.image_neg_Ioc {G : Type u} [ordered_add_comm_group G] (a b : G) :

has_neg.neg '' set.Ioc a b = set.Ico (-b) (-a)

source

theorem set.image_neg_Ioo {G : Type u} [ordered_add_comm_group G] (a b : G) :

has_neg.neg '' set.Ioo a b = set.Ioo (-b) (-a)

source

@[simp]

theorem set.image_const_sub_Ici {G : Type u} [ordered_add_comm_group G] (a b : G) :

(λ (x : G), a - x) '' set.Ici b = set.Iic (a - b)

source

@[simp]

theorem set.image_const_sub_Iic {G : Type u} [ordered_add_comm_group G] (a b : G) :

(λ (x : G), a - x) '' set.Iic b = set.Ici (a - b)

source

@[simp]

theorem set.image_const_sub_Ioi {G : Type u} [ordered_add_comm_group G] (a b : G) :

(λ (x : G), a - x) '' set.Ioi b = set.Iio (a - b)

source

@[simp]

theorem set.image_const_sub_Iio {G : Type u} [ordered_add_comm_group G] (a b : G) :

(λ (x : G), a - x) '' set.Iio b = set.Ioi (a - b)

source

@[simp]

theorem set.image_const_sub_Icc {G : Type u} [ordered_add_comm_group G] (a b c : G) :

(λ (x : G), a - x) '' set.Icc b c = set.Icc (a - c) (a - b)

source

@[simp]

theorem set.image_const_sub_Ico {G : Type u} [ordered_add_comm_group G] (a b c : G) :

(λ (x : G), a - x) '' set.Ico b c = set.Ioc (a - c) (a - b)

source

@[simp]

theorem set.image_const_sub_Ioc {G : Type u} [ordered_add_comm_group G] (a b c : G) :

(λ (x : G), a - x) '' set.Ioc b c = set.Ico (a - c) (a - b)

source

@[simp]

theorem set.image_const_sub_Ioo {G : Type u} [ordered_add_comm_group G] (a b c : G) :

(λ (x : G), a - x) '' set.Ioo b c = set.Ioo (a - c) (a - b)

source

@[simp]

theorem set.image_sub_const_Ici {G : Type u} [ordered_add_comm_group G] (a b : G) :

(λ (x : G), x - a) '' set.Ici b = set.Ici (b - a)

source

@[simp]

theorem set.image_sub_const_Iic {G : Type u} [ordered_add_comm_group G] (a b : G) :

(λ (x : G), x - a) '' set.Iic b = set.Iic (b - a)

source

@[simp]

theorem set.image_sub_const_Ioi {G : Type u} [ordered_add_comm_group G] (a b : G) :

(λ (x : G), x - a) '' set.Ioi b = set.Ioi (b - a)

source

@[simp]

theorem set.image_sub_const_Iio {G : Type u} [ordered_add_comm_group G] (a b : G) :

(λ (x : G), x - a) '' set.Iio b = set.Iio (b - a)

source

@[simp]

theorem set.image_sub_const_Icc {G : Type u} [ordered_add_comm_group G] (a b c : G) :

(λ (x : G), x - a) '' set.Icc b c = set.Icc (b - a) (c - a)

source

@[simp]

theorem set.image_sub_const_Ico {G : Type u} [ordered_add_comm_group G] (a b c : G) :

(λ (x : G), x - a) '' set.Ico b c = set.Ico (b - a) (c - a)

source

@[simp]

theorem set.image_sub_const_Ioc {G : Type u} [ordered_add_comm_group G] (a b c : G) :

(λ (x : G), x - a) '' set.Ioc b c = set.Ioc (b - a) (c - a)

source

@[simp]

theorem set.image_sub_const_Ioo {G : Type u} [ordered_add_comm_group G] (a b c : G) :

(λ (x : G), x - a) '' set.Ioo b c = set.Ioo (b - a) (c - a)

source

@[simp]

theorem set.preimage_mul_const_Iio {k : Type u} [linear_ordered_field k] (a : k) {c : k} :

0 < c → (λ (x : k), x * c) ⁻¹' set.Iio a = set.Iio (a / c)

source

@[simp]

theorem set.preimage_mul_const_Ioi {k : Type u} [linear_ordered_field k] (a : k) {c : k} :

0 < c → (λ (x : k), x * c) ⁻¹' set.Ioi a = set.Ioi (a / c)

source

@[simp]

theorem set.preimage_mul_const_Iic {k : Type u} [linear_ordered_field k] (a : k) {c : k} :

0 < c → (λ (x : k), x * c) ⁻¹' set.Iic a = set.Iic (a / c)

source

@[simp]

theorem set.preimage_mul_const_Ici {k : Type u} [linear_ordered_field k] (a : k) {c : k} :

0 < c → (λ (x : k), x * c) ⁻¹' set.Ici a = set.Ici (a / c)

source

@[simp]

theorem set.preimage_mul_const_Ioo {k : Type u} [linear_ordered_field k] (a b : k) {c : k} :

0 < c → (λ (x : k), x * c) ⁻¹' set.Ioo a b = set.Ioo (a / c) (b / c)

source

@[simp]

theorem set.preimage_mul_const_Ioc {k : Type u} [linear_ordered_field k] (a b : k) {c : k} :

0 < c → (λ (x : k), x * c) ⁻¹' set.Ioc a b = set.Ioc (a / c) (b / c)

source

@[simp]

theorem set.preimage_mul_const_Ico {k : Type u} [linear_ordered_field k] (a b : k) {c : k} :

0 < c → (λ (x : k), x * c) ⁻¹' set.Ico a b = set.Ico (a / c) (b / c)

source

@[simp]

theorem set.preimage_mul_const_Icc {k : Type u} [linear_ordered_field k] (a b : k) {c : k} :

0 < c → (λ (x : k), x * c) ⁻¹' set.Icc a b = set.Icc (a / c) (b / c)

source

@[simp]

theorem set.preimage_mul_const_Iio_of_neg {k : Type u} [linear_ordered_field k] (a : k) {c : k} :

c < 0 → (λ (x : k), x * c) ⁻¹' set.Iio a = set.Ioi (a / c)

source

@[simp]

theorem set.preimage_mul_const_Ioi_of_neg {k : Type u} [linear_ordered_field k] (a : k) {c : k} :

c < 0 → (λ (x : k), x * c) ⁻¹' set.Ioi a = set.Iio (a / c)

source

@[simp]

theorem set.preimage_mul_const_Iic_of_neg {k : Type u} [linear_ordered_field k] (a : k) {c : k} :

c < 0 → (λ (x : k), x * c) ⁻¹' set.Iic a = set.Ici (a / c)

source

@[simp]

theorem set.preimage_mul_const_Ici_of_neg {k : Type u} [linear_ordered_field k] (a : k) {c : k} :

c < 0 → (λ (x : k), x * c) ⁻¹' set.Ici a = set.Iic (a / c)

source

@[simp]

theorem set.preimage_mul_const_Ioo_of_neg {k : Type u} [linear_ordered_field k] (a b : k) {c : k} :

c < 0 → (λ (x : k), x * c) ⁻¹' set.Ioo a b = set.Ioo (b / c) (a / c)

source

@[simp]

theorem set.preimage_mul_const_Ioc_of_neg {k : Type u} [linear_ordered_field k] (a b : k) {c : k} :

c < 0 → (λ (x : k), x * c) ⁻¹' set.Ioc a b = set.Ico (b / c) (a / c)

source

@[simp]

theorem set.preimage_mul_const_Ico_of_neg {k : Type u} [linear_ordered_field k] (a b : k) {c : k} :

c < 0 → (λ (x : k), x * c) ⁻¹' set.Ico a b = set.Ioc (b / c) (a / c)

source

@[simp]

theorem set.preimage_mul_const_Icc_of_neg {k : Type u} [linear_ordered_field k] (a b : k) {c : k} :

c < 0 → (λ (x : k), x * c) ⁻¹' set.Icc a b = set.Icc (b / c) (a / c)

source

@[simp]

theorem set.preimage_const_mul_Iio {k : Type u} [linear_ordered_field k] (a : k) {c : k} :

0 < c → has_mul.mul c ⁻¹' set.Iio a = set.Iio (a / c)

source

@[simp]

theorem set.preimage_const_mul_Ioi {k : Type u} [linear_ordered_field k] (a : k) {c : k} :

0 < c → has_mul.mul c ⁻¹' set.Ioi a = set.Ioi (a / c)

source

@[simp]

theorem set.preimage_const_mul_Iic {k : Type u} [linear_ordered_field k] (a : k) {c : k} :

0 < c → has_mul.mul c ⁻¹' set.Iic a = set.Iic (a / c)

source

@[simp]

theorem set.preimage_const_mul_Ici {k : Type u} [linear_ordered_field k] (a : k) {c : k} :

0 < c → has_mul.mul c ⁻¹' set.Ici a = set.Ici (a / c)

source

@[simp]

theorem set.preimage_const_mul_Ioo {k : Type u} [linear_ordered_field k] (a b : k) {c : k} :

0 < c → has_mul.mul c ⁻¹' set.Ioo a b = set.Ioo (a / c) (b / c)

source

@[simp]

theorem set.preimage_const_mul_Ioc {k : Type u} [linear_ordered_field k] (a b : k) {c : k} :

0 < c → has_mul.mul c ⁻¹' set.Ioc a b = set.Ioc (a / c) (b / c)

source

@[simp]

theorem set.preimage_const_mul_Ico {k : Type u} [linear_ordered_field k] (a b : k) {c : k} :

0 < c → has_mul.mul c ⁻¹' set.Ico a b = set.Ico (a / c) (b / c)

source

@[simp]

theorem set.preimage_const_mul_Icc {k : Type u} [linear_ordered_field k] (a b : k) {c : k} :

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 {k : Type u} [linear_ordered_field k] (a : k) {c : k} :

c < 0 → has_mul.mul c ⁻¹' set.Iio a = set.Ioi (a / c)

source

@[simp]

theorem set.preimage_const_mul_Ioi_of_neg {k : Type u} [linear_ordered_field k] (a : k) {c : k} :

c < 0 → has_mul.mul c ⁻¹' set.Ioi a = set.Iio (a / c)

source

@[simp]

theorem set.preimage_const_mul_Iic_of_neg {k : Type u} [linear_ordered_field k] (a : k) {c : k} :

c < 0 → has_mul.mul c ⁻¹' set.Iic a = set.Ici (a / c)

source

@[simp]

theorem set.preimage_const_mul_Ici_of_neg {k : Type u} [linear_ordered_field k] (a : k) {c : k} :

c < 0 → has_mul.mul c ⁻¹' set.Ici a = set.Iic (a / c)

source

@[simp]

theorem set.preimage_const_mul_Ioo_of_neg {k : Type u} [linear_ordered_field k] (a b : k) {c : k} :

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 {k : Type u} [linear_ordered_field k] (a b : k) {c : k} :

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 {k : Type u} [linear_ordered_field k] (a b : k) {c : k} :

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 {k : Type u} [linear_ordered_field k] (a b : k) {c : k} :

c < 0 → has_mul.mul c ⁻¹' set.Icc a b = set.Icc (b / c) (a / c)

source

theorem set.image_mul_right_Icc' {k : Type u} [linear_ordered_field k] (a b : k) {c : k} :

0 < c → (λ (x : k), x * c) '' set.Icc a b = set.Icc (a * c) (b * c)

source

theorem set.image_mul_right_Icc {k : Type u} [linear_ordered_field k] {a b c : k} :

a ≤ b → 0 ≤ c → (λ (x : k), x * c) '' set.Icc a b = set.Icc (a * c) (b * c)

source

theorem set.image_mul_left_Icc' {k : Type u} [linear_ordered_field k] {a : k} (h : 0 < a) (b c : k) :

has_mul.mul a '' set.Icc b c = set.Icc (a * b) (a * c)

source

theorem set.image_mul_left_Icc {k : Type u} [linear_ordered_field k] {a b c : k} :

0 ≤ a → b ≤ c → has_mul.mul a '' set.Icc b c = set.Icc (a * b) (a * c)

source

theorem set.image_inv_Ioo_0_left {k : Type u} [linear_ordered_field k] {a : k} :

0 < a → has_inv.inv '' set.Ioo 0 a = set.Ioi a⁻¹

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

mathlib documentation

data.set.intervals.image_preimage

(Pre)images of intervals

Preimages under `x ↦ a + x`

Preimages under `x ↦ x + a`

Preimages under `x ↦ -x`

Preimages under `x ↦ x - a`

Preimages under `x ↦ a - x`

Images under `x ↦ a + x`

Images under `x ↦ x + a`

Images under `x ↦ -x`

Images under `x ↦ a - x`

Images under `x ↦ x - a`

Multiplication and inverse in a field

General documentation

Additional documentation

Library

mathlib documentation

data.​set.​intervals.​image_preimage

(Pre)images of intervals

Preimages under x ↦ a + x

Preimages under x ↦ x + a

Preimages under x ↦ -x

Preimages under x ↦ x - a

Preimages under x ↦ a - x

Images under x ↦ a + x

Images under x ↦ x + a

Images under x ↦ -x

Images under x ↦ a - x

Images under x ↦ x - a

Multiplication and inverse in a field

General documentation

Additional documentation

Library

data.set.intervals.image_preimage

Preimages under `x ↦ a + x`

Preimages under `x ↦ x + a`

Preimages under `x ↦ -x`

Preimages under `x ↦ x - a`

Preimages under `x ↦ a - x`

Images under `x ↦ a + x`

Images under `x ↦ x + a`

Images under `x ↦ -x`

Images under `x ↦ a - x`

Images under `x ↦ x - a`