Documentation

Mathlib.Order.Interval.Set.Image

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