Documentation

Mathlib.Data.Set.Intervals.Image

Lemmas about monotone functions on intervals, and intervals in subtypes. #

theorem Monotone.mapsTo_Icc {α : Type u_1} {β : Type u_2} {f : αβ} [Preorder α] [Preorder β] {a : α} {b : α} (h : Monotone f) :
Set.MapsTo f (Set.Icc a b) (Set.Icc (f a) (f b))
theorem StrictMono.mapsTo_Ioo {α : Type u_1} {β : Type u_2} {f : αβ} [Preorder α] [Preorder β] {a : α} {b : α} (h : StrictMono f) :
Set.MapsTo f (Set.Ioo a b) (Set.Ioo (f a) (f b))
theorem Monotone.mapsTo_Ici {α : Type u_1} {β : Type u_2} {f : αβ} [Preorder α] [Preorder β] {a : α} (h : Monotone f) :
Set.MapsTo f (Set.Ici a) (Set.Ici (f a))
theorem Monotone.mapsTo_Iic {α : Type u_1} {β : Type u_2} {f : αβ} [Preorder α] [Preorder β] {a : α} (h : Monotone f) :
Set.MapsTo f (Set.Iic a) (Set.Iic (f a))
theorem StrictMono.mapsTo_Ioi {α : Type u_1} {β : Type u_2} {f : αβ} [Preorder α] [Preorder β] {a : α} (h : StrictMono f) :
Set.MapsTo f (Set.Ioi a) (Set.Ioi (f a))
theorem StrictMono.mapsTo_Iio {α : Type u_1} {β : Type u_2} {f : αβ} [Preorder α] [Preorder β] {a : α} (h : StrictMono f) :
Set.MapsTo f (Set.Iio a) (Set.Iio (f a))
theorem StrictMono.mapsTo_Ico {α : Type u_1} {β : Type u_2} {f : αβ} [PartialOrder α] [Preorder β] {a : α} {b : α} (h : StrictMono f) :
Set.MapsTo f (Set.Ico a b) (Set.Ico (f a) (f b))
theorem StrictMono.mapsTo_Ioc {α : Type u_1} {β : Type u_2} {f : αβ} [PartialOrder α] [Preorder β] {a : α} {b : α} (h : StrictMono f) :
Set.MapsTo f (Set.Ioc a b) (Set.Ioc (f a) (f b))
theorem Monotone.image_Icc_subset {α : Type u_1} {β : Type u_2} {f : αβ} [Preorder α] [Preorder β] {a : α} {b : α} (h : Monotone f) :
f '' Set.Icc a b Set.Icc (f a) (f b)
theorem StrictMono.image_Ioo_subset {α : Type u_1} {β : Type u_2} {f : αβ} [Preorder α] [Preorder β] {a : α} {b : α} (h : StrictMono f) :
f '' Set.Ioo a b Set.Ioo (f a) (f b)
theorem Monotone.image_Ici_subset {α : Type u_1} {β : Type u_2} {f : αβ} [Preorder α] [Preorder β] {a : α} (h : Monotone f) :
f '' Set.Ici a Set.Ici (f a)
theorem Monotone.image_Iic_subset {α : Type u_1} {β : Type u_2} {f : αβ} [Preorder α] [Preorder β] {a : α} (h : Monotone f) :
f '' Set.Iic a Set.Iic (f a)
theorem StrictMono.image_Ioi_subset {α : Type u_1} {β : Type u_2} {f : αβ} [Preorder α] [Preorder β] {a : α} (h : StrictMono f) :
f '' Set.Ioi a Set.Ioi (f a)
theorem StrictMono.image_Iio_subset {α : Type u_1} {β : Type u_2} {f : αβ} [Preorder α] [Preorder β] {a : α} (h : StrictMono f) :
f '' Set.Iio a Set.Iio (f a)
theorem StrictMono.imageIco_subset {α : Type u_1} {β : Type u_2} {f : αβ} [PartialOrder α] [Preorder β] {a : α} {b : α} (h : StrictMono f) :
f '' Set.Ico a b Set.Ico (f a) (f b)
theorem StrictMono.imageIoc_subset {α : Type u_1} {β : Type u_2} {f : αβ} [PartialOrder α] [Preorder β] {a : α} {b : α} (h : StrictMono f) :
f '' Set.Ioc a b Set.Ioc (f a) (f b)
theorem Set.image_subtype_val_Icc_subset {α : Type u_1} [Preorder α] {p : αProp} (a : { x // p x }) (b : { x // p x }) :
Subtype.val '' Set.Icc a b Set.Icc a b
theorem Set.image_subtype_val_Ico_subset {α : Type u_1} [Preorder α] {p : αProp} (a : { x // p x }) (b : { x // p x }) :
Subtype.val '' Set.Ico a b Set.Ico a b
theorem Set.image_subtype_val_Ioc_subset {α : Type u_1} [Preorder α] {p : αProp} (a : { x // p x }) (b : { x // p x }) :
Subtype.val '' Set.Ioc a b Set.Ioc a b
theorem Set.image_subtype_val_Ioo_subset {α : Type u_1} [Preorder α] {p : αProp} (a : { x // p x }) (b : { x // p x }) :
Subtype.val '' Set.Ioo a b Set.Ioo a b
theorem Set.image_subtype_val_Iic_subset {α : Type u_1} [Preorder α] {p : αProp} (a : { x // p x }) :
Subtype.val '' Set.Iic a Set.Iic a
theorem Set.image_subtype_val_Iio_subset {α : Type u_1} [Preorder α] {p : αProp} (a : { x // p x }) :
Subtype.val '' Set.Iio a Set.Iio a
theorem Set.image_subtype_val_Ici_subset {α : Type u_1} [Preorder α] {p : αProp} (a : { x // p x }) :
Subtype.val '' Set.Ici a Set.Ici a
theorem Set.image_subtype_val_Ioi_subset {α : Type u_1} [Preorder α] {p : αProp} (a : { x // p x }) :
Subtype.val '' Set.Ioi a Set.Ioi a