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
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))
:
theorem
StrictMonoOn.image_Ioc_subset
{α : Type u_1}
{β : Type u_2}
{f : α → β}
[PartialOrder α]
[Preorder β]
{a b : α}
(h : StrictMonoOn f (Set.Icc a b))
:
theorem
StrictAntiOn.image_Ico_subset
{α : Type u_1}
{β : Type u_2}
{f : α → β}
[PartialOrder α]
[Preorder β]
{a b : α}
(h : StrictAntiOn f (Set.Icc a b))
:
theorem
StrictAntiOn.image_Ioc_subset
{α : Type u_1}
{β : Type u_2}
{f : α → β}
[PartialOrder α]
[Preorder β]
{a b : α}
(h : StrictAntiOn f (Set.Icc a b))
:
theorem
StrictMono.image_Ico_subset
{α : Type u_1}
{β : Type u_2}
{f : α → β}
[PartialOrder α]
[Preorder β]
{a b : α}
(h : StrictMono f)
:
theorem
StrictMono.image_Ioc_subset
{α : Type u_1}
{β : Type u_2}
{f : α → β}
[PartialOrder α]
[Preorder β]
{a b : α}
(h : StrictMono f)
:
theorem
StrictAnti.image_Ico_subset
{α : Type u_1}
{β : Type u_2}
{f : α → β}
[PartialOrder α]
[Preorder β]
{a b : α}
(h : StrictAnti f)
:
theorem
StrictAnti.image_Ioc_subset
{α : Type u_1}
{β : Type u_2}
{f : α → β}
[PartialOrder α]
[Preorder β]
{a b : α}
(h : StrictAnti f)
:
@[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 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 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 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 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 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 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 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 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)