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.

source
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))
source
theorem MonotoneOn.mapsTo_Iic {α : Type u_1} {β : Type u_2} {f : α → β} [Preorder α] [Preorder β] {a : α} (h : MonotoneOn f (Set.Iic a)) :
Set.MapsTo f (Set.Iic a) (Set.Iic (f a))
source
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))
source
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))
source
theorem AntitoneOn.mapsTo_Iic {α : Type u_1} {β : Type u_2} {f : α → β} [Preorder α] [Preorder β] {a : α} (h : AntitoneOn f (Set.Iic a)) :
Set.MapsTo f (Set.Iic a) (Set.Ici (f a))
source
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))
source
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))
source
theorem StrictMonoOn.mapsTo_Iio {α : Type u_1} {β : Type u_2} {f : α → β} [Preorder α] [Preorder β] {a : α} (h : StrictMonoOn f (Set.Iic a)) :
Set.MapsTo f (Set.Iio a) (Set.Iio (f a))
source
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))
source
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))
source
theorem StrictAntiOn.mapsTo_Iio {α : Type u_1} {β : Type u_2} {f : α → β} [Preorder α] [Preorder β] {a : α} (h : StrictAntiOn f (Set.Iic a)) :
Set.MapsTo f (Set.Iio a) (Set.Ioi (f a))
source
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))
source
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))
source
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))
source
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))
source
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))
source
theorem Antitone.mapsTo_Iic {α : Type u_1} {β : Type u_2} {f : α → β} [Preorder α] [Preorder β] {a : α} (h : Antitone f) :
Set.MapsTo f (Set.Iic a) (Set.Ici (f a))
source
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))
source
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))
source
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))
source
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))
source
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))
source
theorem StrictAnti.mapsTo_Iio {α : Type u_1} {β : Type u_2} {f : α → β} [Preorder α] [Preorder β] {a : α} (h : StrictAnti f) :
Set.MapsTo f (Set.Iio a) (Set.Ioi (f a))
source
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))
source
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)
source
theorem MonotoneOn.image_Iic_subset {α : Type u_1} {β : Type u_2} {f : α → β} [Preorder α] [Preorder β] {a : α} (h : MonotoneOn f (Set.Iic a)) :
f '' Set.Iic a ⊆ Set.Iic (f a)
source
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)
source
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)
source
theorem AntitoneOn.image_Iic_subset {α : Type u_1} {β : Type u_2} {f : α → β} [Preorder α] [Preorder β] {a : α} (h : AntitoneOn f (Set.Iic a)) :
f '' Set.Iic a ⊆ Set.Ici (f a)
source
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)
source
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)
source
theorem StrictMonoOn.image_Iio_subset {α : Type u_1} {β : Type u_2} {f : α → β} [Preorder α] [Preorder β] {a : α} (h : StrictMonoOn f (Set.Iic a)) :
f '' Set.Iio a ⊆ Set.Iio (f a)
source
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)
source
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)
source
theorem StrictAntiOn.image_Iio_subset {α : Type u_1} {β : Type u_2} {f : α → β} [Preorder α] [Preorder β] {a : α} (h : StrictAntiOn f (Set.Iic a)) :
f '' Set.Iio a ⊆ Set.Ioi (f a)
source
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)
source
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)
source
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)
source
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)
source
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)
source
theorem Antitone.image_Iic_subset {α : Type u_1} {β : Type u_2} {f : α → β} [Preorder α] [Preorder β] {a : α} (h : Antitone f) :
f '' Set.Iic a ⊆ Set.Ici (f a)
source
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)
source
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)
source
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)
source
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)
source
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)
source
theorem StrictAnti.image_Iio_subset {α : Type u_1} {β : Type u_2} {f : α → β} [Preorder α] [Preorder β] {a : α} (h : StrictAnti f) :
f '' Set.Iio a ⊆ Set.Ioi (f a)
source
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)
source
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))
source
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))
source
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))
source
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))
source
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))
source
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))
source
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))
source
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))
source
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)
source
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)
source
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)
source
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)
source
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)
source
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)
source
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)
source
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)
source
@[simp]
theorem Set.preimage_subtype_val_Ici {α : Type u_1} [Preorder α] {p : α → Prop} (a : { x : α // p x }) :
Subtype.val ⁻¹' Ici ↑a = Ici a
source
@[simp]
theorem Set.preimage_subtype_val_Iic {α : Type u_1} [Preorder α] {p : α → Prop} (a : { x : α // p x }) :
Subtype.val ⁻¹' Iic ↑a = Iic a
source
@[simp]
theorem Set.preimage_subtype_val_Ioi {α : Type u_1} [Preorder α] {p : α → Prop} (a : { x : α // p x }) :
Subtype.val ⁻¹' Ioi ↑a = Ioi a
source
@[simp]
theorem Set.preimage_subtype_val_Iio {α : Type u_1} [Preorder α] {p : α → Prop} (a : { x : α // p x }) :
Subtype.val ⁻¹' Iio ↑a = Iio a
source
@[simp]
theorem Set.preimage_subtype_val_Icc {α : Type u_1} [Preorder α] {p : α → Prop} (a b : { x : α // p x }) :
Subtype.val ⁻¹' Icc ↑a ↑b = Icc a b
source
@[simp]
theorem Set.preimage_subtype_val_Ico {α : Type u_1} [Preorder α] {p : α → Prop} (a b : { x : α // p x }) :
Subtype.val ⁻¹' Ico ↑a ↑b = Ico a b
source
@[simp]
theorem Set.preimage_subtype_val_Ioc {α : Type u_1} [Preorder α] {p : α → Prop} (a b : { x : α // p x }) :
Subtype.val ⁻¹' Ioc ↑a ↑b = Ioc a b
source
@[simp]
theorem Set.preimage_subtype_val_Ioo {α : Type u_1} [Preorder α] {p : α → Prop} (a b : { x : α // p x }) :
Subtype.val ⁻¹' Ioo ↑a ↑b = Ioo a b
source
theorem Set.image_subtype_val_Icc_subset {α : Type u_1} [Preorder α] {p : α → Prop} (a b : { x : α // p x }) :
Subtype.val '' Icc a b ⊆ Icc ↑a ↑b
source
theorem Set.image_subtype_val_Ico_subset {α : Type u_1} [Preorder α] {p : α → Prop} (a b : { x : α // p x }) :
Subtype.val '' Ico a b ⊆ Ico ↑a ↑b
source
theorem Set.image_subtype_val_Ioc_subset {α : Type u_1} [Preorder α] {p : α → Prop} (a b : { x : α // p x }) :
Subtype.val '' Ioc a b ⊆ Ioc ↑a ↑b
source
theorem Set.image_subtype_val_Ioo_subset {α : Type u_1} [Preorder α] {p : α → Prop} (a b : { x : α // p x }) :
Subtype.val '' Ioo a b ⊆ Ioo ↑a ↑b
source
theorem Set.image_subtype_val_Iic_subset {α : Type u_1} [Preorder α] {p : α → Prop} (a : { x : α // p x }) :
Subtype.val '' Iic a ⊆ Iic ↑a
source
theorem Set.image_subtype_val_Ici_subset {α : Type u_1} [Preorder α] {p : α → Prop} (a : { x : α // p x }) :
Subtype.val '' Ici a ⊆ Ici ↑a
source
theorem Set.image_subtype_val_Iio_subset {α : Type u_1} [Preorder α] {p : α → Prop} (a : { x : α // p x }) :
Subtype.val '' Iio a ⊆ Iio ↑a
source
theorem Set.image_subtype_val_Ioi_subset {α : Type u_1} [Preorder α] {p : α → Prop} (a : { x : α // p x }) :
Subtype.val '' Ioi a ⊆ Ioi ↑a
source
@[simp]
theorem Set.image_subtype_val_Ici_Iic {α : Type u_1} [Preorder α] {a : α} (b : ↑(Ici a)) :
Subtype.val '' Iic b = Icc a ↑b
source
@[simp]
theorem Set.image_subtype_val_Iic_Ici {α : Type u_1} [Preorder α] {a : α} (b : ↑(Iic a)) :
Subtype.val '' Ici b = Icc (↑b) a
source
@[simp]
theorem Set.image_subtype_val_Ici_Iio {α : Type u_1} [Preorder α] {a : α} (b : ↑(Ici a)) :
Subtype.val '' Iio b = Ico a ↑b
source
@[simp]
theorem Set.image_subtype_val_Iic_Ioi {α : Type u_1} [Preorder α] {a : α} (b : ↑(Iic a)) :
Subtype.val '' Ioi b = Ioc (↑b) a
source
@[simp]
theorem Set.image_subtype_val_Ici_Ici {α : Type u_1} [Preorder α] {a : α} (b : ↑(Ici a)) :
Subtype.val '' Ici b = Ici ↑b
source
@[simp]
theorem Set.image_subtype_val_Iic_Iic {α : Type u_1} [Preorder α] {a : α} (b : ↑(Iic a)) :
Subtype.val '' Iic b = Iic ↑b
source
@[simp]
theorem Set.image_subtype_val_Ici_Ioi {α : Type u_1} [Preorder α] {a : α} (b : ↑(Ici a)) :
Subtype.val '' Ioi b = Ioi ↑b
source
@[simp]
theorem Set.image_subtype_val_Iic_Iio {α : Type u_1} [Preorder α] {a : α} (b : ↑(Iic a)) :
Subtype.val '' Iio b = Iio ↑b
source
@[simp]
theorem Set.image_subtype_val_Ioi_Ici {α : Type u_1} [Preorder α] {a : α} (b : ↑(Ioi a)) :
Subtype.val '' Ici b = Ici ↑b
source
@[simp]
theorem Set.image_subtype_val_Iio_Iic {α : Type u_1} [Preorder α] {a : α} (b : ↑(Iio a)) :
Subtype.val '' Iic b = Iic ↑b
source
@[simp]
theorem Set.image_subtype_val_Ioi_Iic {α : Type u_1} [Preorder α] {a : α} (b : ↑(Ioi a)) :
Subtype.val '' Iic b = Ioc a ↑b
source
@[simp]
theorem Set.image_subtype_val_Iio_Ici {α : Type u_1} [Preorder α] {a : α} (b : ↑(Iio a)) :
Subtype.val '' Ici b = Ico (↑b) a
source
@[simp]
theorem Set.image_subtype_val_Ioi_Ioi {α : Type u_1} [Preorder α] {a : α} (b : ↑(Ioi a)) :
Subtype.val '' Ioi b = Ioi ↑b
source
@[simp]
theorem Set.image_subtype_val_Iio_Iio {α : Type u_1} [Preorder α] {a : α} (b : ↑(Iio a)) :
Subtype.val '' Iio b = Iio ↑b
source
@[simp]
theorem Set.image_subtype_val_Ioi_Iio {α : Type u_1} [Preorder α] {a : α} (b : ↑(Ioi a)) :
Subtype.val '' Iio b = Ioo a ↑b
source
@[simp]
theorem Set.image_subtype_val_Iio_Ioi {α : Type u_1} [Preorder α] {a : α} (b : ↑(Iio a)) :
Subtype.val '' Ioi b = Ioo (↑b) a
source
@[simp]
theorem Set.image_subtype_val_Icc_Ici {α : Type u_1} [Preorder α] {a b : α} (c : ↑(Icc a b)) :
Subtype.val '' Ici c = Icc (↑c) b
source
@[simp]
theorem Set.image_subtype_val_Icc_Iic {α : Type u_1} [Preorder α] {a b : α} (c : ↑(Icc a b)) :
Subtype.val '' Iic c = Icc a ↑c
source
@[simp]
theorem Set.image_subtype_val_Icc_Ioi {α : Type u_1} [Preorder α] {a b : α} (c : ↑(Icc a b)) :
Subtype.val '' Ioi c = Ioc (↑c) b
source
@[simp]
theorem Set.image_subtype_val_Icc_Iio {α : Type u_1} [Preorder α] {a b : α} (c : ↑(Icc a b)) :
Subtype.val '' Iio c = Ico a ↑c
source
@[simp]
theorem Set.image_subtype_val_Ico_Ici {α : Type u_1} [Preorder α] {a b : α} (c : ↑(Ico a b)) :
Subtype.val '' Ici c = Ico (↑c) b
source
@[simp]
theorem Set.image_subtype_val_Ioc_Iic {α : Type u_1} [Preorder α] {a b : α} (c : ↑(Ioc a b)) :
Subtype.val '' Iic c = Ioc a ↑c
source
@[simp]
theorem Set.image_subtype_val_Ioc_Ici {α : Type u_1} [Preorder α] {a b : α} (c : ↑(Ioc a b)) :
Subtype.val '' Ici c = Icc (↑c) b
source
@[simp]
theorem Set.image_subtype_val_Ico_Iic {α : Type u_1} [Preorder α] {a b : α} (c : ↑(Ico a b)) :
Subtype.val '' Iic c = Icc a ↑c
source
@[simp]
theorem Set.image_subtype_val_Ico_Ioi {α : Type u_1} [Preorder α] {a b : α} (c : ↑(Ico a b)) :
Subtype.val '' Ioi c = Ioo (↑c) b
source
@[simp]
theorem Set.image_subtype_val_Ioc_Iio {α : Type u_1} [Preorder α] {a b : α} (c : ↑(Ioc a b)) :
Subtype.val '' Iio c = Ioo a ↑c
source
@[simp]
theorem Set.image_subtype_val_Ioc_Ioi {α : Type u_1} [Preorder α] {a b : α} (c : ↑(Ioc a b)) :
Subtype.val '' Ioi c = Ioc (↑c) b
source
@[simp]
theorem Set.image_subtype_val_Ico_Iio {α : Type u_1} [Preorder α] {a b : α} (c : ↑(Ico a b)) :
Subtype.val '' Iio c = Ico a ↑c
source
@[simp]
theorem Set.image_subtype_val_Ioo_Ici {α : Type u_1} [Preorder α] {a b : α} (c : ↑(Ioo a b)) :
Subtype.val '' Ici c = Ico (↑c) b
source
@[simp]
theorem Set.image_subtype_val_Ioo_Iic {α : Type u_1} [Preorder α] {a b : α} (c : ↑(Ioo a b)) :
Subtype.val '' Iic c = Ioc a ↑c
source
@[simp]
theorem Set.image_subtype_val_Ioo_Ioi {α : Type u_1} [Preorder α] {a b : α} (c : ↑(Ioo a b)) :
Subtype.val '' Ioi c = Ioo (↑c) b
source
@[simp]
theorem Set.image_subtype_val_Ioo_Iio {α : Type u_1} [Preorder α] {a b : α} (c : ↑(Ioo a b)) :
Subtype.val '' Iio c = Ioo a ↑c
source
theorem directedOn_le_Iic {α : Type u_1} [Preorder α] (a : α) :
DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) (Set.Iic a)
source
theorem directedOn_ge_Ici {α : Type u_1} [Preorder α] (a : α) :
DirectedOn (fun (x1 x2 : α) => x2 ≤ x1) (Set.Ici a)
source
theorem directedOn_le_Icc {α : Type u_1} [Preorder α] (a b : α) :
DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) (Set.Icc a b)
source
theorem directedOn_ge_Icc {α : Type u_1} [Preorder α] (a b : α) :
DirectedOn (fun (x1 x2 : α) => x2 ≤ x1) (Set.Icc a b)
source
theorem directedOn_le_Ioc {α : Type u_1} [Preorder α] (a b : α) :
DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) (Set.Ioc a b)
source
theorem directedOn_ge_Ico {α : Type u_1} [Preorder α] (a b : α) :
DirectedOn (fun (x1 x2 : α) => x2 ≤ x1) (Set.Ico a b)