Skip to content

Commit

Permalink
feat(Data/Set/Intervals/Image): Complete API (#7146)
Browse files Browse the repository at this point in the history 
Dualise all existing lemmas and prove their strictly monotone versions.

The lemmas are grouped as
* `mapsTo`, `image_subset`
  * `On`, not `On`
    * `Monotone`, `Antitone`, `StrictMono`, `StrictAnti`
      * `Ixi`, `Iix`, `Ixx`




Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
  • Loading branch information
@YaelDillies @eric-wieser
YaelDillies and eric-wieser committed Sep 28, 2023
1 parent b86770a commit dae39b2
Show file tree
Hide file tree
Showing 3 changed files with 259 additions and 57 deletions.
248 changes: 193 additions & 55 deletions Mathlib/Data/Set/Intervals/Image.lean
View file
@@ -1,12 +1,16 @@
/-
Copyright (c) 2023 Kim Liesinger. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Kim Liesinger
Authors: Kim Liesinger, Yaël Dillies
-/
import Mathlib.Data.Set.Intervals.Basic
import Mathlib.Data.Set.Function

/-! ### Lemmas about monotone functions on intervals, and intervals in subtypes.
/-!
# 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`.
-/

set_option autoImplicit true
Expand All @@ -15,90 +19,224 @@ variable {f : α → β}

open Set

section
variable [Preorder α] [Preorder β]
section Preorder
variable [Preorder α] [Preorder β] {a b : α}

lemma MonotoneOn.mapsTo_Ici (h : MonotoneOn f (Ici a)) : MapsTo f (Ici a) (Ici (f a)) :=
fun _ _ ↦ by aesop

lemma MonotoneOn.mapsTo_Iic (h : MonotoneOn f (Iic b)) : MapsTo f (Iic b) (Iic (f b)) :=
fun _ _ ↦ by aesop

lemma MonotoneOn.mapsTo_Icc (h : MonotoneOn f (Icc a b)) : MapsTo f (Icc a b) (Icc (f a) (f b)) :=
fun _c hc ↦
⟨h (left_mem_Icc.2 <| hc.1.trans hc.2) hc hc.1, h hc (right_mem_Icc.2 <| hc.1.trans hc.2) hc.2⟩

lemma AntitoneOn.mapsTo_Ici (h : AntitoneOn f (Ici a)) : MapsTo f (Ici a) (Iic (f a)) :=
fun _ _ ↦ by aesop

lemma AntitoneOn.mapsTo_Iic (h : AntitoneOn f (Iic b)) : MapsTo f (Iic b) (Ici (f b)) :=
fun _ _ ↦ by aesop

lemma AntitoneOn.mapsTo_Icc (h : AntitoneOn f (Icc a b)) : MapsTo f (Icc a b) (Icc (f b) (f a)) :=
fun _c hc ↦
⟨h hc (right_mem_Icc.2 <| hc.1.trans hc.2) hc.2, h (left_mem_Icc.2 <| hc.1.trans hc.2) hc hc.1⟩

lemma StrictMonoOn.mapsTo_Ioi (h : StrictMonoOn f (Ici a)) : MapsTo f (Ioi a) (Ioi (f a)) :=
fun _c hc ↦ h le_rfl hc.le hc

theorem Monotone.mapsTo_Icc (h : Monotone f) :
MapsTo f (Icc a b) (Icc (f a) (f b)) :=
fun _ _ => by aesop
lemma StrictMonoOn.mapsTo_Iio (h : StrictMonoOn f (Iic b)) : MapsTo f (Iio b) (Iio (f b)) :=
fun _c hc ↦ h hc.le le_rfl hc

theorem StrictMono.mapsTo_Ioo (h : StrictMono f) :
lemma StrictMonoOn.mapsTo_Ioo (h : StrictMonoOn f (Icc a b)) :
MapsTo f (Ioo a b) (Ioo (f a) (f b)) :=
fun _ _ => by aesop
fun _c hc ↦
⟨h (left_mem_Icc.2 (hc.1.trans hc.2).le) (Ioo_subset_Icc_self hc) hc.1,
h (Ioo_subset_Icc_self hc) (right_mem_Icc.2 (hc.1.trans hc.2).le) hc.2⟩

theorem Monotone.mapsTo_Ici (h : Monotone f) :
MapsTo f (Ici a) (Ici (f a)) :=
fun _ _ => by aesop
lemma StrictAntiOn.mapsTo_Ioi (h : StrictAntiOn f (Ici a)) : MapsTo f (Ioi a) (Iio (f a)) :=
fun _c hc ↦ h le_rfl hc.le hc

theorem Monotone.mapsTo_Iic (h : Monotone f) :
MapsTo f (Iic a) (Iic (f a)) :=
fun _ _ => by aesop
lemma StrictAntiOn.mapsTo_Iio (h : StrictAntiOn f (Iic b)) : MapsTo f (Iio b) (Ioi (f b)) :=
fun _c hc ↦ h hc.le le_rfl hc

theorem StrictMono.mapsTo_Ioi (h : StrictMono f) :
MapsTo f (Ioi a) (Ioi (f a)) :=
fun _ _ => by aesop
lemma StrictAntiOn.mapsTo_Ioo (h : StrictAntiOn f (Icc a b)) :
MapsTo f (Ioo a b) (Ioo (f b) (f a)) :=
fun _c hc ↦
⟨h (Ioo_subset_Icc_self hc) (right_mem_Icc.2 (hc.1.trans hc.2).le) hc.2,
h (left_mem_Icc.2 (hc.1.trans hc.2).le) (Ioo_subset_Icc_self hc) hc.1⟩

theorem StrictMono.mapsTo_Iio (h : StrictMono f) :
MapsTo f (Iio a) (Iio (f a)) :=
fun _ _ => by aesop
lemma Monotone.mapsTo_Ici (h : Monotone f) : MapsTo f (Ici a) (Ici (f a)) :=
(h.monotoneOn _).mapsTo_Ici

end
lemma Monotone.mapsTo_Iic (h : Monotone f) : MapsTo f (Iic b) (Iic (f b)) :=
(h.monotoneOn _).mapsTo_Iic

section
variable [PartialOrder α] [Preorder β]
lemma Monotone.mapsTo_Icc (h : Monotone f) : MapsTo f (Icc a b) (Icc (f a) (f b)) :=
(h.monotoneOn _).mapsTo_Icc

theorem StrictMono.mapsTo_Ico (h : StrictMono f) :
MapsTo f (Ico a b) (Ico (f a) (f b)) :=
-- It makes me sad that `aesop` doesn't do this. There are clearly missing lemmas.
fun _ m => ⟨h.monotone m.1, h m.2⟩
lemma Antitone.mapsTo_Ici (h : Antitone f) : MapsTo f (Ici a) (Iic (f a)) :=
(h.antitoneOn _).mapsTo_Ici

theorem StrictMono.mapsTo_Ioc (h : StrictMono f) :
MapsTo f (Ioc a b) (Ioc (f a) (f b)) :=
fun _ m => ⟨h m.1, h.monotone m.2⟩
lemma Antitone.mapsTo_Iic (h : Antitone f) : MapsTo f (Iic b) (Ici (f b)) :=
(h.antitoneOn _).mapsTo_Iic

end
lemma Antitone.mapsTo_Icc (h : Antitone f) : MapsTo f (Icc a b) (Icc (f b) (f a)) :=
(h.antitoneOn _).mapsTo_Icc

section
variable [Preorder α] [Preorder β]
lemma StrictMono.mapsTo_Ioi (h : StrictMono f) : MapsTo f (Ioi a) (Ioi (f a)) :=
(h.strictMonoOn _).mapsTo_Ioi

theorem Monotone.image_Icc_subset (h : Monotone f) :
f '' Icc a b ⊆ Icc (f a) (f b) :=
h.mapsTo_Icc.image_subset
lemma StrictMono.mapsTo_Iio (h : StrictMono f) : MapsTo f (Iio b) (Iio (f b)) :=
(h.strictMonoOn _).mapsTo_Iio

lemma StrictMono.mapsTo_Ioo (h : StrictMono f) : MapsTo f (Ioo a b) (Ioo (f a) (f b)) :=
(h.strictMonoOn _).mapsTo_Ioo

lemma StrictAnti.mapsTo_Ioi (h : StrictAnti f) : MapsTo f (Ioi a) (Iio (f a)) :=
(h.strictAntiOn _).mapsTo_Ioi

lemma StrictAnti.mapsTo_Iio (h : StrictAnti f) : MapsTo f (Iio b) (Ioi (f b)) :=
(h.strictAntiOn _).mapsTo_Iio

theorem StrictMono.image_Ioo_subset (h : StrictMono f) :
f '' Ioo a b ⊆ Ioo (f a) (f b) :=
h.mapsTo_Ioo.image_subset
lemma StrictAnti.mapsTo_Ioo (h : StrictAnti f) : MapsTo f (Ioo a b) (Ioo (f b) (f a)) :=
(h.strictAntiOn _).mapsTo_Ioo

theorem Monotone.image_Ici_subset (h : Monotone f) :
f '' Ici a ⊆ Ici (f a) :=
lemma MonotoneOn.image_Ici_subset (h : MonotoneOn f (Ici a)) : f '' Ici a ⊆ Ici (f a) :=
h.mapsTo_Ici.image_subset

theorem Monotone.image_Iic_subset (h : Monotone f) :
f '' Iic a ⊆ Iic (f a) :=
lemma MonotoneOn.image_Iic_subset (h : MonotoneOn f (Iic b)) : f '' Iic b ⊆ Iic (f b) :=
h.mapsTo_Iic.image_subset

theorem StrictMono.image_Ioi_subset (h : StrictMono f) :
f '' Ioi a ⊆ Ioi (f a) :=
lemma MonotoneOn.image_Icc_subset (h : MonotoneOn f (Icc a b)) : f '' Icc a b ⊆ Icc (f a) (f b) :=
h.mapsTo_Icc.image_subset

lemma AntitoneOn.image_Ici_subset (h : AntitoneOn f (Ici a)) : f '' Ici a ⊆ Iic (f a) :=
h.mapsTo_Ici.image_subset

lemma AntitoneOn.image_Iic_subset (h : AntitoneOn f (Iic b)) : f '' Iic b ⊆ Ici (f b) :=
h.mapsTo_Iic.image_subset

lemma AntitoneOn.image_Icc_subset (h : AntitoneOn f (Icc a b)) : f '' Icc a b ⊆ Icc (f b) (f a) :=
h.mapsTo_Icc.image_subset

lemma StrictMonoOn.image_Ioi_subset (h : StrictMonoOn f (Ici a)) : f '' Ioi a ⊆ Ioi (f a) :=
h.mapsTo_Ioi.image_subset

theorem StrictMono.image_Iio_subset (h : StrictMono f) :
f '' Iio a ⊆ Iio (f a) :=
lemma StrictMonoOn.image_Iio_subset (h : StrictMonoOn f (Iic b)) : f '' Iio b ⊆ Iio (f b) :=
h.mapsTo_Iio.image_subset

end
lemma StrictMonoOn.image_Ioo_subset (h : StrictMonoOn f (Icc a b)) :
f '' Ioo a b ⊆ Ioo (f a) (f b) := h.mapsTo_Ioo.image_subset

lemma StrictAntiOn.image_Ioi_subset (h : StrictAntiOn f (Ici a)) : f '' Ioi a ⊆ Iio (f a) :=
h.mapsTo_Ioi.image_subset

lemma StrictAntiOn.image_Iio_subset (h : StrictAntiOn f (Iic b)) : f '' Iio b ⊆ Ioi (f b) :=
h.mapsTo_Iio.image_subset

lemma StrictAntiOn.image_Ioo_subset (h : StrictAntiOn f (Icc a b)) :
f '' Ioo a b ⊆ Ioo (f b) (f a) := h.mapsTo_Ioo.image_subset

lemma Monotone.image_Ici_subset (h : Monotone f) : f '' Ici a ⊆ Ici (f a) :=
(h.monotoneOn _).image_Ici_subset

section
lemma Monotone.image_Iic_subset (h : Monotone f) : f '' Iic b ⊆ Iic (f b) :=
(h.monotoneOn _).image_Iic_subset

lemma Monotone.image_Icc_subset (h : Monotone f) : f '' Icc a b ⊆ Icc (f a) (f b) :=
(h.monotoneOn _).image_Icc_subset

lemma Antitone.image_Ici_subset (h : Antitone f) : f '' Ici a ⊆ Iic (f a) :=
(h.antitoneOn _).image_Ici_subset

lemma Antitone.image_Iic_subset (h : Antitone f) : f '' Iic b ⊆ Ici (f b) :=
(h.antitoneOn _).image_Iic_subset

lemma Antitone.image_Icc_subset (h : Antitone f) : f '' Icc a b ⊆ Icc (f b) (f a) :=
(h.antitoneOn _).image_Icc_subset

lemma StrictMono.image_Ioi_subset (h : StrictMono f) : f '' Ioi a ⊆ Ioi (f a) :=
(h.strictMonoOn _).image_Ioi_subset

lemma StrictMono.image_Iio_subset (h : StrictMono f) : f '' Iio b ⊆ Iio (f b) :=
(h.strictMonoOn _).image_Iio_subset

lemma StrictMono.image_Ioo_subset (h : StrictMono f) : f '' Ioo a b ⊆ Ioo (f a) (f b) :=
(h.strictMonoOn _).image_Ioo_subset

lemma StrictAnti.image_Ioi_subset (h : StrictAnti f) : f '' Ioi a ⊆ Iio (f a) :=
(h.strictAntiOn _).image_Ioi_subset

lemma StrictAnti.image_Iio_subset (h : StrictAnti f) : f '' Iio b ⊆ Ioi (f b) :=
(h.strictAntiOn _).image_Iio_subset

lemma StrictAnti.image_Ioo_subset (h : StrictAnti f) : f '' Ioo a b ⊆ Ioo (f b) (f a) :=
(h.strictAntiOn _).image_Ioo_subset

end Preorder

section PartialOrder
variable [PartialOrder α] [Preorder β]

theorem StrictMono.imageIco_subset (h : StrictMono f) :
f '' Ico a b ⊆ Ico (f a) (f b) :=
h.mapsTo_Ico.image_subset
lemma StrictMonoOn.mapsTo_Ico (h : StrictMonoOn f (Icc a b)) :
MapsTo f (Ico a b) (Ico (f a) (f b)) :=
fun _c hc ↦ ⟨h.monotoneOn (left_mem_Icc.2 <| hc.1.trans hc.2.le) (Ico_subset_Icc_self hc) hc.1,
h (Ico_subset_Icc_self hc) (right_mem_Icc.2 <| hc.1.trans hc.2.le) hc.2⟩

lemma StrictMonoOn.mapsTo_Ioc (h : StrictMonoOn f (Icc a b)) :
MapsTo f (Ioc a b) (Ioc (f a) (f b)) :=
fun _c hc ↦ ⟨h (left_mem_Icc.2 <| hc.1.le.trans hc.2) (Ioc_subset_Icc_self hc) hc.1,
h.monotoneOn (Ioc_subset_Icc_self hc) (right_mem_Icc.2 <| hc.1.le.trans hc.2) hc.2⟩

lemma StrictAntiOn.mapsTo_Ico (h : StrictAntiOn f (Icc a b)) :
MapsTo f (Ico a b) (Ioc (f b) (f a)) :=
fun _c hc ↦ ⟨h (Ico_subset_Icc_self hc) (right_mem_Icc.2 <| hc.1.trans hc.2.le) hc.2,
h.antitoneOn (left_mem_Icc.2 <| hc.1.trans hc.2.le) (Ico_subset_Icc_self hc) hc.1⟩

lemma StrictAntiOn.mapsTo_Ioc (h : StrictAntiOn f (Icc a b)) :
MapsTo f (Ioc a b) (Ico (f b) (f a)) :=
fun _c hc ↦ ⟨h.antitoneOn (Ioc_subset_Icc_self hc) (right_mem_Icc.2 <| hc.1.le.trans hc.2) hc.2,
h (left_mem_Icc.2 <| hc.1.le.trans hc.2) (Ioc_subset_Icc_self hc) hc.1⟩

lemma StrictMono.mapsTo_Ico (h : StrictMono f) : MapsTo f (Ico a b) (Ico (f a) (f b)) :=
(h.strictMonoOn _).mapsTo_Ico

lemma StrictMono.mapsTo_Ioc (h : StrictMono f) : MapsTo f (Ioc a b) (Ioc (f a) (f b)) :=
(h.strictMonoOn _).mapsTo_Ioc

lemma StrictAnti.mapsTo_Ico (h : StrictAnti f) : MapsTo f (Ico a b) (Ioc (f b) (f a)) :=
(h.strictAntiOn _).mapsTo_Ico

lemma StrictAnti.mapsTo_Ioc (h : StrictAnti f) : MapsTo f (Ioc a b) (Ico (f b) (f a)) :=
(h.strictAntiOn _).mapsTo_Ioc

theorem StrictMono.imageIoc_subset (h : StrictMono f) :
lemma StrictMonoOn.image_Ico_subset (h : StrictMonoOn f (Icc a b)) :
f '' Ico a b ⊆ Ico (f a) (f b) := h.mapsTo_Ico.image_subset

lemma StrictMonoOn.image_Ioc_subset (h : StrictMonoOn f (Icc a b)) :
f '' Ioc a b ⊆ Ioc (f a) (f b) :=
h.mapsTo_Ioc.image_subset

end
lemma StrictAntiOn.image_Ico_subset (h : StrictAntiOn f (Icc a b)) :
f '' Ico a b ⊆ Ioc (f b) (f a) := h.mapsTo_Ico.image_subset

lemma StrictAntiOn.image_Ioc_subset (h : StrictAntiOn f (Icc a b)) :
f '' Ioc a b ⊆ Ico (f b) (f a) := h.mapsTo_Ioc.image_subset

lemma StrictMono.image_Ico_subset (h : StrictMono f) : f '' Ico a b ⊆ Ico (f a) (f b) :=
(h.strictMonoOn _).image_Ico_subset

lemma StrictMono.image_Ioc_subset (h : StrictMono f) : f '' Ioc a b ⊆ Ioc (f a) (f b) :=
(h.strictMonoOn _).image_Ioc_subset

lemma StrictAnti.image_Ico_subset (h : StrictAnti f) : f '' Ico a b ⊆ Ioc (f b) (f a) :=
(h.strictAntiOn _).image_Ico_subset

lemma StrictAnti.image_Ioc_subset (h : StrictAnti f) : f '' Ioc a b ⊆ Ico (f b) (f a) :=
(h.strictAntiOn _).image_Ioc_subset

end PartialOrder

namespace Set

Expand Down
38 changes: 36 additions & 2 deletions Mathlib/Data/Set/Intervals/UnorderedInterval.lean
View file
Expand Up @@ -3,8 +3,8 @@ Copyright (c) 2020 Zhouhang Zhou. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Zhouhang Zhou
-/
import Mathlib.Data.Set.Intervals.Image
import Mathlib.Order.Bounds.Basic
import Mathlib.Data.Set.Intervals.Basic
import Mathlib.Tactic.Common

#align_import data.set.intervals.unordered_interval from "leanprover-community/mathlib"@"4020ddee5b4580a409bfda7d2f42726ce86ae674"
Expand Down Expand Up @@ -180,8 +180,42 @@ lemma uIcc_injective_left (a : α) : Injective (uIcc a) := by
end DistribLattice

section LinearOrder
variable [LinearOrder α]

variable [LinearOrder α] [LinearOrder β] {f : α → β} {s : Set α} {a a₁ a₂ b b₁ b₂ c x : α}
section Lattice
variable [Lattice β] {f : α → β} {s : Set α} {a b : α}

lemma _root_.MonotoneOn.mapsTo_uIcc (hf : MonotoneOn f (uIcc a b)) :
MapsTo f (uIcc a b) (uIcc (f a) (f b)) := by
rw [uIcc, uIcc, ←hf.map_sup, ←hf.map_inf] <;>
apply_rules [left_mem_uIcc, right_mem_uIcc, hf.mapsTo_Icc]

lemma _root_.AntitoneOn.mapsTo_uIcc (hf : AntitoneOn f (uIcc a b)) :
MapsTo f (uIcc a b) (uIcc (f a) (f b)) := by
rw [uIcc, uIcc, ←hf.map_sup, ←hf.map_inf] <;>
apply_rules [left_mem_uIcc, right_mem_uIcc, hf.mapsTo_Icc]

lemma _root_.Monotone.mapsTo_uIcc (hf : Monotone f) : MapsTo f (uIcc a b) (uIcc (f a) (f b)) :=
(hf.monotoneOn _).mapsTo_uIcc

lemma _root_.Antitone.mapsTo_uIcc (hf : Antitone f) : MapsTo f (uIcc a b) (uIcc (f a) (f b)) :=
(hf.antitoneOn _).mapsTo_uIcc

lemma _root_.MonotoneOn.image_uIcc_subset (hf : MonotoneOn f (uIcc a b)) :
f '' uIcc a b ⊆ uIcc (f a) (f b) := hf.mapsTo_uIcc.image_subset

lemma _root_.AntitoneOn.image_uIcc_subset (hf : AntitoneOn f (uIcc a b)) :
f '' uIcc a b ⊆ uIcc (f a) (f b) := hf.mapsTo_uIcc.image_subset

lemma _root_.Monotone.image_uIcc_subset (hf : Monotone f) : f '' uIcc a b ⊆ uIcc (f a) (f b) :=
(hf.monotoneOn _).image_uIcc_subset

lemma _root_.Antitone.image_uIcc_subset (hf : Antitone f) : f '' uIcc a b ⊆ uIcc (f a) (f b) :=
(hf.antitoneOn _).image_uIcc_subset

end Lattice

variable [LinearOrder β] {f : α → β} {s : Set α} {a a₁ a₂ b b₁ b₂ c d x : α}

theorem Icc_min_max : Icc (min a b) (max a b) = [[a, b]] :=
rfl
Expand Down

0 comments on commit dae39b2

Please sign in to comment.