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 ⁻¹' Ici ↑a = Ici a
@[simp]
theorem
Set.preimage_subtype_val_Iic
{α : Type u_1}
[Preorder α]
{p : α → Prop}
(a : { x : α // p x })
:
Subtype.val ⁻¹' Iic ↑a = Iic a
@[simp]
theorem
Set.preimage_subtype_val_Ioi
{α : Type u_1}
[Preorder α]
{p : α → Prop}
(a : { x : α // p x })
:
Subtype.val ⁻¹' Ioi ↑a = Ioi a
@[simp]
theorem
Set.preimage_subtype_val_Iio
{α : Type u_1}
[Preorder α]
{p : α → Prop}
(a : { x : α // p x })
:
Subtype.val ⁻¹' Iio ↑a = Iio a
@[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
@[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
@[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
@[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
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
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
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
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
theorem
Set.image_subtype_val_Iic_subset
{α : Type u_1}
[Preorder α]
{p : α → Prop}
(a : { x : α // p x })
:
Subtype.val '' Iic a ⊆ Iic ↑a
theorem
Set.image_subtype_val_Iio_subset
{α : Type u_1}
[Preorder α]
{p : α → Prop}
(a : { x : α // p x })
:
Subtype.val '' Iio a ⊆ Iio ↑a
theorem
Set.image_subtype_val_Ici_subset
{α : Type u_1}
[Preorder α]
{p : α → Prop}
(a : { x : α // p x })
:
Subtype.val '' Ici a ⊆ Ici ↑a
theorem
Set.image_subtype_val_Ioi_subset
{α : Type u_1}
[Preorder α]
{p : α → Prop}
(a : { x : α // p x })
:
Subtype.val '' Ioi a ⊆ Ioi ↑a
@[simp]
theorem
Set.image_subtype_val_Ici_Iic
{α : Type u_1}
[Preorder α]
{a : α}
(b : ↑(Ici a))
:
Subtype.val '' Iic b = Icc a ↑b
@[simp]
theorem
Set.image_subtype_val_Ici_Iio
{α : Type u_1}
[Preorder α]
{a : α}
(b : ↑(Ici a))
:
Subtype.val '' Iio b = Ico a ↑b
@[simp]
theorem
Set.image_subtype_val_Ici_Ici
{α : Type u_1}
[Preorder α]
{a : α}
(b : ↑(Ici a))
:
Subtype.val '' Ici b = Ici ↑b
@[simp]
theorem
Set.image_subtype_val_Ici_Ioi
{α : Type u_1}
[Preorder α]
{a : α}
(b : ↑(Ici a))
:
Subtype.val '' Ioi b = Ioi ↑b
@[simp]
theorem
Set.image_subtype_val_Iic_Ici
{α : Type u_1}
[Preorder α]
{a : α}
(b : ↑(Iic a))
:
Subtype.val '' Ici b = Icc (↑b) a
@[simp]
theorem
Set.image_subtype_val_Iic_Ioi
{α : Type u_1}
[Preorder α]
{a : α}
(b : ↑(Iic a))
:
Subtype.val '' Ioi b = Ioc (↑b) a
@[simp]
theorem
Set.image_subtype_val_Iic_Iic
{α : Type u_1}
[Preorder α]
{a : α}
(b : ↑(Iic a))
:
Subtype.val '' Iic b = Iic ↑b
@[simp]
theorem
Set.image_subtype_val_Iic_Iio
{α : Type u_1}
[Preorder α]
{a : α}
(b : ↑(Iic a))
:
Subtype.val '' Iio b = Iio ↑b
@[simp]
theorem
Set.image_subtype_val_Ioi_Ici
{α : Type u_1}
[Preorder α]
{a : α}
(b : ↑(Ioi a))
:
Subtype.val '' Ici b = Ici ↑b
@[simp]
theorem
Set.image_subtype_val_Ioi_Iic
{α : Type u_1}
[Preorder α]
{a : α}
(b : ↑(Ioi a))
:
Subtype.val '' Iic b = Ioc a ↑b
@[simp]
theorem
Set.image_subtype_val_Ioi_Ioi
{α : Type u_1}
[Preorder α]
{a : α}
(b : ↑(Ioi a))
:
Subtype.val '' Ioi b = Ioi ↑b
@[simp]
theorem
Set.image_subtype_val_Ioi_Iio
{α : Type u_1}
[Preorder α]
{a : α}
(b : ↑(Ioi a))
:
Subtype.val '' Iio b = Ioo a ↑b
@[simp]
theorem
Set.image_subtype_val_Iio_Ici
{α : Type u_1}
[Preorder α]
{a : α}
(b : ↑(Iio a))
:
Subtype.val '' Ici b = Ico (↑b) a
@[simp]
theorem
Set.image_subtype_val_Iio_Iic
{α : Type u_1}
[Preorder α]
{a : α}
(b : ↑(Iio a))
:
Subtype.val '' Iic b = Iic ↑b
@[simp]
theorem
Set.image_subtype_val_Iio_Ioi
{α : Type u_1}
[Preorder α]
{a : α}
(b : ↑(Iio a))
:
Subtype.val '' Ioi b = Ioo (↑b) a
@[simp]
theorem
Set.image_subtype_val_Iio_Iio
{α : Type u_1}
[Preorder α]
{a : α}
(b : ↑(Iio a))
:
Subtype.val '' Iio b = Iio ↑b
@[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
@[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
@[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
@[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
@[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
@[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
@[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
@[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
@[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
@[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
@[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
@[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
@[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
@[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
@[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
@[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
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)