# Monotone functions on intervals #

This file shows many variants of the fact that a monotone function f sends an interval with endpoints a and b to the interval with endpoints f a and f b.

theorem MonotoneOn.mapsTo_Ici {α : Type u_1} {β : Type u_2} {f : αβ} [] [] {a : α} (h : MonotoneOn f (Set.Ici a)) :
Set.MapsTo f (Set.Ici a) (Set.Ici (f a))
theorem MonotoneOn.mapsTo_Iic {α : Type u_1} {β : Type u_2} {f : αβ} [] [] {b : α} (h : MonotoneOn f (Set.Iic b)) :
Set.MapsTo f (Set.Iic b) (Set.Iic (f b))
theorem MonotoneOn.mapsTo_Icc {α : Type u_1} {β : Type u_2} {f : αβ} [] [] {a : α} {b : α} (h : MonotoneOn f (Set.Icc a b)) :
Set.MapsTo f (Set.Icc a b) (Set.Icc (f a) (f b))
theorem AntitoneOn.mapsTo_Ici {α : Type u_1} {β : Type u_2} {f : αβ} [] [] {a : α} (h : AntitoneOn f (Set.Ici a)) :
Set.MapsTo f (Set.Ici a) (Set.Iic (f a))
theorem AntitoneOn.mapsTo_Iic {α : Type u_1} {β : Type u_2} {f : αβ} [] [] {b : α} (h : AntitoneOn f (Set.Iic b)) :
Set.MapsTo f (Set.Iic b) (Set.Ici (f b))
theorem AntitoneOn.mapsTo_Icc {α : Type u_1} {β : Type u_2} {f : αβ} [] [] {a : α} {b : α} (h : AntitoneOn f (Set.Icc a b)) :
Set.MapsTo f (Set.Icc a b) (Set.Icc (f b) (f a))
theorem StrictMonoOn.mapsTo_Ioi {α : Type u_1} {β : Type u_2} {f : αβ} [] [] {a : α} (h : StrictMonoOn f (Set.Ici a)) :
Set.MapsTo f (Set.Ioi a) (Set.Ioi (f a))
theorem StrictMonoOn.mapsTo_Iio {α : Type u_1} {β : Type u_2} {f : αβ} [] [] {b : α} (h : StrictMonoOn f (Set.Iic b)) :
Set.MapsTo f (Set.Iio b) (Set.Iio (f b))
theorem StrictMonoOn.mapsTo_Ioo {α : Type u_1} {β : Type u_2} {f : αβ} [] [] {a : α} {b : α} (h : StrictMonoOn f (Set.Icc a b)) :
Set.MapsTo f (Set.Ioo a b) (Set.Ioo (f a) (f b))
theorem StrictAntiOn.mapsTo_Ioi {α : Type u_1} {β : Type u_2} {f : αβ} [] [] {a : α} (h : StrictAntiOn f (Set.Ici a)) :
Set.MapsTo f (Set.Ioi a) (Set.Iio (f a))
theorem StrictAntiOn.mapsTo_Iio {α : Type u_1} {β : Type u_2} {f : αβ} [] [] {b : α} (h : StrictAntiOn f (Set.Iic b)) :
Set.MapsTo f (Set.Iio b) (Set.Ioi (f b))
theorem StrictAntiOn.mapsTo_Ioo {α : Type u_1} {β : Type u_2} {f : αβ} [] [] {a : α} {b : α} (h : StrictAntiOn f (Set.Icc a b)) :
Set.MapsTo f (Set.Ioo a b) (Set.Ioo (f b) (f a))
theorem Monotone.mapsTo_Ici {α : Type u_1} {β : Type u_2} {f : αβ} [] [] {a : α} (h : ) :
Set.MapsTo f (Set.Ici a) (Set.Ici (f a))
theorem Monotone.mapsTo_Iic {α : Type u_1} {β : Type u_2} {f : αβ} [] [] {b : α} (h : ) :
Set.MapsTo f (Set.Iic b) (Set.Iic (f b))
theorem Monotone.mapsTo_Icc {α : Type u_1} {β : Type u_2} {f : αβ} [] [] {a : α} {b : α} (h : ) :
Set.MapsTo f (Set.Icc a b) (Set.Icc (f a) (f b))
theorem Antitone.mapsTo_Ici {α : Type u_1} {β : Type u_2} {f : αβ} [] [] {a : α} (h : ) :
Set.MapsTo f (Set.Ici a) (Set.Iic (f a))
theorem Antitone.mapsTo_Iic {α : Type u_1} {β : Type u_2} {f : αβ} [] [] {b : α} (h : ) :
Set.MapsTo f (Set.Iic b) (Set.Ici (f b))
theorem Antitone.mapsTo_Icc {α : Type u_1} {β : Type u_2} {f : αβ} [] [] {a : α} {b : α} (h : ) :
Set.MapsTo f (Set.Icc a b) (Set.Icc (f b) (f a))
theorem StrictMono.mapsTo_Ioi {α : Type u_1} {β : Type u_2} {f : αβ} [] [] {a : α} (h : ) :
Set.MapsTo f (Set.Ioi a) (Set.Ioi (f a))
theorem StrictMono.mapsTo_Iio {α : Type u_1} {β : Type u_2} {f : αβ} [] [] {b : α} (h : ) :
Set.MapsTo f (Set.Iio b) (Set.Iio (f b))
theorem StrictMono.mapsTo_Ioo {α : Type u_1} {β : Type u_2} {f : αβ} [] [] {a : α} {b : α} (h : ) :
Set.MapsTo f (Set.Ioo a b) (Set.Ioo (f a) (f b))
theorem StrictAnti.mapsTo_Ioi {α : Type u_1} {β : Type u_2} {f : αβ} [] [] {a : α} (h : ) :
Set.MapsTo f (Set.Ioi a) (Set.Iio (f a))
theorem StrictAnti.mapsTo_Iio {α : Type u_1} {β : Type u_2} {f : αβ} [] [] {b : α} (h : ) :
Set.MapsTo f (Set.Iio b) (Set.Ioi (f b))
theorem StrictAnti.mapsTo_Ioo {α : Type u_1} {β : Type u_2} {f : αβ} [] [] {a : α} {b : α} (h : ) :
Set.MapsTo f (Set.Ioo a b) (Set.Ioo (f b) (f a))
theorem MonotoneOn.image_Ici_subset {α : Type u_1} {β : Type u_2} {f : αβ} [] [] {a : α} (h : MonotoneOn f (Set.Ici a)) :
f '' Set.Ici (f a)
theorem MonotoneOn.image_Iic_subset {α : Type u_1} {β : Type u_2} {f : αβ} [] [] {b : α} (h : MonotoneOn f (Set.Iic b)) :
f '' Set.Iic (f b)
theorem MonotoneOn.image_Icc_subset {α : Type u_1} {β : Type u_2} {f : αβ} [] [] {a : α} {b : α} (h : MonotoneOn f (Set.Icc a b)) :
f '' Set.Icc a b Set.Icc (f a) (f b)
theorem AntitoneOn.image_Ici_subset {α : Type u_1} {β : Type u_2} {f : αβ} [] [] {a : α} (h : AntitoneOn f (Set.Ici a)) :
f '' Set.Iic (f a)
theorem AntitoneOn.image_Iic_subset {α : Type u_1} {β : Type u_2} {f : αβ} [] [] {b : α} (h : AntitoneOn f (Set.Iic b)) :
f '' Set.Ici (f b)
theorem AntitoneOn.image_Icc_subset {α : Type u_1} {β : Type u_2} {f : αβ} [] [] {a : α} {b : α} (h : AntitoneOn f (Set.Icc a b)) :
f '' Set.Icc a b Set.Icc (f b) (f a)
theorem StrictMonoOn.image_Ioi_subset {α : Type u_1} {β : Type u_2} {f : αβ} [] [] {a : α} (h : StrictMonoOn f (Set.Ici a)) :
f '' Set.Ioi (f a)
theorem StrictMonoOn.image_Iio_subset {α : Type u_1} {β : Type u_2} {f : αβ} [] [] {b : α} (h : StrictMonoOn f (Set.Iic b)) :
f '' Set.Iio (f b)
theorem StrictMonoOn.image_Ioo_subset {α : Type u_1} {β : Type u_2} {f : αβ} [] [] {a : α} {b : α} (h : StrictMonoOn f (Set.Icc a b)) :
f '' Set.Ioo a b Set.Ioo (f a) (f b)
theorem StrictAntiOn.image_Ioi_subset {α : Type u_1} {β : Type u_2} {f : αβ} [] [] {a : α} (h : StrictAntiOn f (Set.Ici a)) :
f '' Set.Iio (f a)
theorem StrictAntiOn.image_Iio_subset {α : Type u_1} {β : Type u_2} {f : αβ} [] [] {b : α} (h : StrictAntiOn f (Set.Iic b)) :
f '' Set.Ioi (f b)
theorem StrictAntiOn.image_Ioo_subset {α : Type u_1} {β : Type u_2} {f : αβ} [] [] {a : α} {b : α} (h : StrictAntiOn f (Set.Icc a b)) :
f '' Set.Ioo a b Set.Ioo (f b) (f a)
theorem Monotone.image_Ici_subset {α : Type u_1} {β : Type u_2} {f : αβ} [] [] {a : α} (h : ) :
f '' Set.Ici (f a)
theorem Monotone.image_Iic_subset {α : Type u_1} {β : Type u_2} {f : αβ} [] [] {b : α} (h : ) :
f '' Set.Iic (f b)
theorem Monotone.image_Icc_subset {α : Type u_1} {β : Type u_2} {f : αβ} [] [] {a : α} {b : α} (h : ) :
f '' Set.Icc a b Set.Icc (f a) (f b)
theorem Antitone.image_Ici_subset {α : Type u_1} {β : Type u_2} {f : αβ} [] [] {a : α} (h : ) :
f '' Set.Iic (f a)
theorem Antitone.image_Iic_subset {α : Type u_1} {β : Type u_2} {f : αβ} [] [] {b : α} (h : ) :
f '' Set.Ici (f b)
theorem Antitone.image_Icc_subset {α : Type u_1} {β : Type u_2} {f : αβ} [] [] {a : α} {b : α} (h : ) :
f '' Set.Icc a b Set.Icc (f b) (f a)
theorem StrictMono.image_Ioi_subset {α : Type u_1} {β : Type u_2} {f : αβ} [] [] {a : α} (h : ) :
f '' Set.Ioi (f a)
theorem StrictMono.image_Iio_subset {α : Type u_1} {β : Type u_2} {f : αβ} [] [] {b : α} (h : ) :
f '' Set.Iio (f b)
theorem StrictMono.image_Ioo_subset {α : Type u_1} {β : Type u_2} {f : αβ} [] [] {a : α} {b : α} (h : ) :
f '' Set.Ioo a b Set.Ioo (f a) (f b)
theorem StrictAnti.image_Ioi_subset {α : Type u_1} {β : Type u_2} {f : αβ} [] [] {a : α} (h : ) :
f '' Set.Iio (f a)
theorem StrictAnti.image_Iio_subset {α : Type u_1} {β : Type u_2} {f : αβ} [] [] {b : α} (h : ) :
f '' Set.Ioi (f b)
theorem StrictAnti.image_Ioo_subset {α : Type u_1} {β : Type u_2} {f : αβ} [] [] {a : α} {b : α} (h : ) :
f '' Set.Ioo a b Set.Ioo (f b) (f a)
theorem StrictMonoOn.mapsTo_Ico {α : Type u_1} {β : Type u_2} {f : αβ} [] [] {a : α} {b : α} (h : StrictMonoOn f (Set.Icc a b)) :
Set.MapsTo f (Set.Ico a b) (Set.Ico (f a) (f b))
theorem StrictMonoOn.mapsTo_Ioc {α : Type u_1} {β : Type u_2} {f : αβ} [] [] {a : α} {b : α} (h : StrictMonoOn f (Set.Icc a b)) :
Set.MapsTo f (Set.Ioc a b) (Set.Ioc (f a) (f b))
theorem StrictAntiOn.mapsTo_Ico {α : Type u_1} {β : Type u_2} {f : αβ} [] [] {a : α} {b : α} (h : StrictAntiOn f (Set.Icc a b)) :
Set.MapsTo f (Set.Ico a b) (Set.Ioc (f b) (f a))
theorem StrictAntiOn.mapsTo_Ioc {α : Type u_1} {β : Type u_2} {f : αβ} [] [] {a : α} {b : α} (h : StrictAntiOn f (Set.Icc a b)) :
Set.MapsTo f (Set.Ioc a b) (Set.Ico (f b) (f a))
theorem StrictMono.mapsTo_Ico {α : Type u_1} {β : Type u_2} {f : αβ} [] [] {a : α} {b : α} (h : ) :
Set.MapsTo f (Set.Ico a b) (Set.Ico (f a) (f b))
theorem StrictMono.mapsTo_Ioc {α : Type u_1} {β : Type u_2} {f : αβ} [] [] {a : α} {b : α} (h : ) :
Set.MapsTo f (Set.Ioc a b) (Set.Ioc (f a) (f b))
theorem StrictAnti.mapsTo_Ico {α : Type u_1} {β : Type u_2} {f : αβ} [] [] {a : α} {b : α} (h : ) :
Set.MapsTo f (Set.Ico a b) (Set.Ioc (f b) (f a))
theorem StrictAnti.mapsTo_Ioc {α : Type u_1} {β : Type u_2} {f : αβ} [] [] {a : α} {b : α} (h : ) :
Set.MapsTo f (Set.Ioc a b) (Set.Ico (f b) (f a))
theorem StrictMonoOn.image_Ico_subset {α : Type u_1} {β : Type u_2} {f : αβ} [] [] {a : α} {b : α} (h : StrictMonoOn f (Set.Icc a b)) :
f '' Set.Ico a b Set.Ico (f a) (f b)
theorem StrictMonoOn.image_Ioc_subset {α : Type u_1} {β : Type u_2} {f : αβ} [] [] {a : α} {b : α} (h : StrictMonoOn f (Set.Icc a b)) :
f '' Set.Ioc a b Set.Ioc (f a) (f b)
theorem StrictAntiOn.image_Ico_subset {α : Type u_1} {β : Type u_2} {f : αβ} [] [] {a : α} {b : α} (h : StrictAntiOn f (Set.Icc a b)) :
f '' Set.Ico a b Set.Ioc (f b) (f a)
theorem StrictAntiOn.image_Ioc_subset {α : Type u_1} {β : Type u_2} {f : αβ} [] [] {a : α} {b : α} (h : StrictAntiOn f (Set.Icc a b)) :
f '' Set.Ioc a b Set.Ico (f b) (f a)
theorem StrictMono.image_Ico_subset {α : Type u_1} {β : Type u_2} {f : αβ} [] [] {a : α} {b : α} (h : ) :
f '' Set.Ico a b Set.Ico (f a) (f b)
theorem StrictMono.image_Ioc_subset {α : Type u_1} {β : Type u_2} {f : αβ} [] [] {a : α} {b : α} (h : ) :
f '' Set.Ioc a b Set.Ioc (f a) (f b)
theorem StrictAnti.image_Ico_subset {α : Type u_1} {β : Type u_2} {f : αβ} [] [] {a : α} {b : α} (h : ) :
f '' Set.Ico a b Set.Ioc (f b) (f a)
theorem StrictAnti.image_Ioc_subset {α : Type u_1} {β : Type u_2} {f : αβ} [] [] {a : α} {b : α} (h : ) :
f '' Set.Ioc a b Set.Ico (f b) (f a)
@[simp]
theorem Set.preimage_subtype_val_Ici {α : Type u_1} [] {p : αProp} (a : { x : α // p x }) :
Subtype.val ⁻¹' Set.Ici a =
@[simp]
theorem Set.preimage_subtype_val_Iic {α : Type u_1} [] {p : αProp} (a : { x : α // p x }) :
Subtype.val ⁻¹' Set.Iic a =
@[simp]
theorem Set.preimage_subtype_val_Ioi {α : Type u_1} [] {p : αProp} (a : { x : α // p x }) :
Subtype.val ⁻¹' Set.Ioi a =
@[simp]
theorem Set.preimage_subtype_val_Iio {α : Type u_1} [] {p : αProp} (a : { x : α // p x }) :
Subtype.val ⁻¹' Set.Iio a =
@[simp]
theorem Set.preimage_subtype_val_Icc {α : Type u_1} [] {p : αProp} (a : { x : α // p x }) (b : { x : α // p x }) :
Subtype.val ⁻¹' Set.Icc a b = Set.Icc a b
@[simp]
theorem Set.preimage_subtype_val_Ico {α : Type u_1} [] {p : αProp} (a : { x : α // p x }) (b : { x : α // p x }) :
Subtype.val ⁻¹' Set.Ico a b = Set.Ico a b
@[simp]
theorem Set.preimage_subtype_val_Ioc {α : Type u_1} [] {p : αProp} (a : { x : α // p x }) (b : { x : α // p x }) :
Subtype.val ⁻¹' Set.Ioc a b = Set.Ioc a b
@[simp]
theorem Set.preimage_subtype_val_Ioo {α : Type u_1} [] {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_Icc_subset {α : Type u_1} [] {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} [] {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} [] {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} [] {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} [] {p : αProp} (a : { x : α // p x }) :
Subtype.val '' Set.Iic a
theorem Set.image_subtype_val_Iio_subset {α : Type u_1} [] {p : αProp} (a : { x : α // p x }) :
Subtype.val '' Set.Iio a
theorem Set.image_subtype_val_Ici_subset {α : Type u_1} [] {p : αProp} (a : { x : α // p x }) :
Subtype.val '' Set.Ici a
theorem Set.image_subtype_val_Ioi_subset {α : Type u_1} [] {p : αProp} (a : { x : α // p x }) :
Subtype.val '' Set.Ioi a
@[simp]
theorem Set.image_subtype_val_Ici_Iic {α : Type u_1} [] {a : α} (b : (Set.Ici a)) :
Subtype.val '' = Set.Icc a b
@[simp]
theorem Set.image_subtype_val_Ici_Iio {α : Type u_1} [] {a : α} (b : (Set.Ici a)) :
Subtype.val '' = Set.Ico a b
@[simp]
theorem Set.image_subtype_val_Ici_Ici {α : Type u_1} [] {a : α} (b : (Set.Ici a)) :
Subtype.val '' = Set.Ici b
@[simp]
theorem Set.image_subtype_val_Ici_Ioi {α : Type u_1} [] {a : α} (b : (Set.Ici a)) :
Subtype.val '' = Set.Ioi b
@[simp]
theorem Set.image_subtype_val_Iic_Ici {α : Type u_1} [] {a : α} (b : (Set.Iic a)) :
Subtype.val '' = Set.Icc (↑b) a
@[simp]
theorem Set.image_subtype_val_Iic_Ioi {α : Type u_1} [] {a : α} (b : (Set.Iic a)) :
Subtype.val '' = Set.Ioc (↑b) a
@[simp]
theorem Set.image_subtype_val_Iic_Iic {α : Type u_1} [] {a : α} (b : (Set.Iic a)) :
Subtype.val '' = Set.Iic b
@[simp]
theorem Set.image_subtype_val_Iic_Iio {α : Type u_1} [] {a : α} (b : (Set.Iic a)) :
Subtype.val '' = Set.Iio b
@[simp]
theorem Set.image_subtype_val_Ioi_Ici {α : Type u_1} [] {a : α} (b : (Set.Ioi a)) :
Subtype.val '' = Set.Ici b
@[simp]
theorem Set.image_subtype_val_Ioi_Iic {α : Type u_1} [] {a : α} (b : (Set.Ioi a)) :
Subtype.val '' = Set.Ioc a b
@[simp]
theorem Set.image_subtype_val_Ioi_Ioi {α : Type u_1} [] {a : α} (b : (Set.Ioi a)) :
Subtype.val '' = Set.Ioi b
@[simp]
theorem Set.image_subtype_val_Ioi_Iio {α : Type u_1} [] {a : α} (b : (Set.Ioi a)) :
Subtype.val '' = Set.Ioo a b
@[simp]
theorem Set.image_subtype_val_Iio_Ici {α : Type u_1} [] {a : α} (b : (Set.Iio a)) :
Subtype.val '' = Set.Ico (↑b) a
@[simp]
theorem Set.image_subtype_val_Iio_Iic {α : Type u_1} [] {a : α} (b : (Set.Iio a)) :
Subtype.val '' = Set.Iic b
@[simp]
theorem Set.image_subtype_val_Iio_Ioi {α : Type u_1} [] {a : α} (b : (Set.Iio a)) :
Subtype.val '' = Set.Ioo (↑b) a
@[simp]
theorem Set.image_subtype_val_Iio_Iio {α : Type u_1} [] {a : α} (b : (Set.Iio a)) :
Subtype.val '' = Set.Iio b
@[simp]
theorem Set.image_subtype_val_Icc_Ici {α : Type u_1} [] {a : α} {b : α} (c : (Set.Icc a b)) :
Subtype.val '' = Set.Icc (↑c) b
@[simp]
theorem Set.image_subtype_val_Icc_Iic {α : Type u_1} [] {a : α} {b : α} (c : (Set.Icc a b)) :
Subtype.val '' = Set.Icc a c
@[simp]
theorem Set.image_subtype_val_Icc_Ioi {α : Type u_1} [] {a : α} {b : α} (c : (Set.Icc a b)) :
Subtype.val '' = Set.Ioc (↑c) b
@[simp]
theorem Set.image_subtype_val_Icc_Iio {α : Type u_1} [] {a : α} {b : α} (c : (Set.Icc a b)) :
Subtype.val '' = Set.Ico a c
@[simp]
theorem Set.image_subtype_val_Ico_Ici {α : Type u_1} [] {a : α} {b : α} (c : (Set.Ico a b)) :
Subtype.val '' = Set.Ico (↑c) b
@[simp]
theorem Set.image_subtype_val_Ico_Iic {α : Type u_1} [] {a : α} {b : α} (c : (Set.Ico a b)) :
Subtype.val '' = Set.Icc a c
@[simp]
theorem Set.image_subtype_val_Ico_Ioi {α : Type u_1} [] {a : α} {b : α} (c : (Set.Ico a b)) :
Subtype.val '' = Set.Ioo (↑c) b
@[simp]
theorem Set.image_subtype_val_Ico_Iio {α : Type u_1} [] {a : α} {b : α} (c : (Set.Ico a b)) :
Subtype.val '' = Set.Ico a c
@[simp]
theorem Set.image_subtype_val_Ioc_Ici {α : Type u_1} [] {a : α} {b : α} (c : (Set.Ioc a b)) :
Subtype.val '' = Set.Icc (↑c) b
@[simp]
theorem Set.image_subtype_val_Ioc_Iic {α : Type u_1} [] {a : α} {b : α} (c : (Set.Ioc a b)) :
Subtype.val '' = Set.Ioc a c
@[simp]
theorem Set.image_subtype_val_Ioc_Ioi {α : Type u_1} [] {a : α} {b : α} (c : (Set.Ioc a b)) :
Subtype.val '' = Set.Ioc (↑c) b
@[simp]
theorem Set.image_subtype_val_Ioc_Iio {α : Type u_1} [] {a : α} {b : α} (c : (Set.Ioc a b)) :
Subtype.val '' = Set.Ioo a c
@[simp]
theorem Set.image_subtype_val_Ioo_Ici {α : Type u_1} [] {a : α} {b : α} (c : (Set.Ioo a b)) :
Subtype.val '' = Set.Ico (↑c) b
@[simp]
theorem Set.image_subtype_val_Ioo_Iic {α : Type u_1} [] {a : α} {b : α} (c : (Set.Ioo a b)) :
Subtype.val '' = Set.Ioc a c
@[simp]
theorem Set.image_subtype_val_Ioo_Ioi {α : Type u_1} [] {a : α} {b : α} (c : (Set.Ioo a b)) :
Subtype.val '' = Set.Ioo (↑c) b
@[simp]
theorem Set.image_subtype_val_Ioo_Iio {α : Type u_1} [] {a : α} {b : α} (c : (Set.Ioo a b)) :
Subtype.val '' = Set.Ioo a c
theorem directedOn_le_Iic {α : Type u_1} [] (b : α) :
DirectedOn (fun (x x_1 : α) => x x_1) (Set.Iic b)
theorem directedOn_le_Icc {α : Type u_1} [] (a : α) (b : α) :
DirectedOn (fun (x x_1 : α) => x x_1) (Set.Icc a b)
theorem directedOn_le_Ioc {α : Type u_1} [] (a : α) (b : α) :
DirectedOn (fun (x x_1 : α) => x x_1) (Set.Ioc a b)
theorem directedOn_ge_Ici {α : Type u_1} [] (a : α) :
DirectedOn (fun (x x_1 : α) => x x_1) (Set.Ici a)
theorem directedOn_ge_Icc {α : Type u_1} [] (a : α) (b : α) :
DirectedOn (fun (x x_1 : α) => x x_1) (Set.Icc a b)
theorem directedOn_ge_Ico {α : Type u_1} [] (a : α) (b : α) :
DirectedOn (fun (x x_1 : α) => x x_1) (Set.Ico a b)