Documentation

Mathlib.Data.Set.Monotone

Monotone functions over sets #

Congruence lemmas for monotonicity and antitonicity #

theorem MonotoneOn.congr {α : Type u_1} {β : Type u_2} {s : Set α} {f₁ : αβ} {f₂ : αβ} [Preorder α] [Preorder β] (h₁ : MonotoneOn f₁ s) (h : Set.EqOn f₁ f₂ s) :
MonotoneOn f₂ s
theorem AntitoneOn.congr {α : Type u_1} {β : Type u_2} {s : Set α} {f₁ : αβ} {f₂ : αβ} [Preorder α] [Preorder β] (h₁ : AntitoneOn f₁ s) (h : Set.EqOn f₁ f₂ s) :
AntitoneOn f₂ s
theorem StrictMonoOn.congr {α : Type u_1} {β : Type u_2} {s : Set α} {f₁ : αβ} {f₂ : αβ} [Preorder α] [Preorder β] (h₁ : StrictMonoOn f₁ s) (h : Set.EqOn f₁ f₂ s) :
theorem StrictAntiOn.congr {α : Type u_1} {β : Type u_2} {s : Set α} {f₁ : αβ} {f₂ : αβ} [Preorder α] [Preorder β] (h₁ : StrictAntiOn f₁ s) (h : Set.EqOn f₁ f₂ s) :
theorem Set.EqOn.congr_monotoneOn {α : Type u_1} {β : Type u_2} {s : Set α} {f₁ : αβ} {f₂ : αβ} [Preorder α] [Preorder β] (h : Set.EqOn f₁ f₂ s) :
MonotoneOn f₁ s MonotoneOn f₂ s
theorem Set.EqOn.congr_antitoneOn {α : Type u_1} {β : Type u_2} {s : Set α} {f₁ : αβ} {f₂ : αβ} [Preorder α] [Preorder β] (h : Set.EqOn f₁ f₂ s) :
AntitoneOn f₁ s AntitoneOn f₂ s
theorem Set.EqOn.congr_strictMonoOn {α : Type u_1} {β : Type u_2} {s : Set α} {f₁ : αβ} {f₂ : αβ} [Preorder α] [Preorder β] (h : Set.EqOn f₁ f₂ s) :
theorem Set.EqOn.congr_strictAntiOn {α : Type u_1} {β : Type u_2} {s : Set α} {f₁ : αβ} {f₂ : αβ} [Preorder α] [Preorder β] (h : Set.EqOn f₁ f₂ s) :

Monotonicity lemmas #

theorem MonotoneOn.mono {α : Type u_1} {β : Type u_2} {s : Set α} {s₂ : Set α} {f : αβ} [Preorder α] [Preorder β] (h : MonotoneOn f s) (h' : s₂ s) :
MonotoneOn f s₂
theorem AntitoneOn.mono {α : Type u_1} {β : Type u_2} {s : Set α} {s₂ : Set α} {f : αβ} [Preorder α] [Preorder β] (h : AntitoneOn f s) (h' : s₂ s) :
AntitoneOn f s₂
theorem StrictMonoOn.mono {α : Type u_1} {β : Type u_2} {s : Set α} {s₂ : Set α} {f : αβ} [Preorder α] [Preorder β] (h : StrictMonoOn f s) (h' : s₂ s) :
theorem StrictAntiOn.mono {α : Type u_1} {β : Type u_2} {s : Set α} {s₂ : Set α} {f : αβ} [Preorder α] [Preorder β] (h : StrictAntiOn f s) (h' : s₂ s) :
theorem MonotoneOn.monotone {α : Type u_1} {β : Type u_2} {s : Set α} {f : αβ} [Preorder α] [Preorder β] (h : MonotoneOn f s) :
Monotone (f Subtype.val)
theorem AntitoneOn.monotone {α : Type u_1} {β : Type u_2} {s : Set α} {f : αβ} [Preorder α] [Preorder β] (h : AntitoneOn f s) :
Antitone (f Subtype.val)
theorem StrictMonoOn.strictMono {α : Type u_1} {β : Type u_2} {s : Set α} {f : αβ} [Preorder α] [Preorder β] (h : StrictMonoOn f s) :
StrictMono (f Subtype.val)
theorem StrictAntiOn.strictAnti {α : Type u_1} {β : Type u_2} {s : Set α} {f : αβ} [Preorder α] [Preorder β] (h : StrictAntiOn f s) :
StrictAnti (f Subtype.val)
theorem Set.MonotoneOn_insert_iff {α : Type u_1} {β : Type u_2} {s : Set α} {f : αβ} [Preorder α] [Preorder β] {a : α} :
MonotoneOn f (insert a s) (∀ bs, b af b f a) (∀ bs, a bf a f b) MonotoneOn f s
theorem Set.AntitoneOn_insert_iff {α : Type u_1} {β : Type u_2} {s : Set α} {f : αβ} [Preorder α] [Preorder β] {a : α} :
AntitoneOn f (insert a s) (∀ bs, b af a f b) (∀ bs, a bf b f a) AntitoneOn f s

Monotone #

theorem Monotone.restrict {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : αβ} (h : Monotone f) (s : Set α) :
Monotone (s.restrict f)
theorem Monotone.codRestrict {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : αβ} (h : Monotone f) {s : Set β} (hs : ∀ (x : α), f x s) :
theorem Monotone.rangeFactorization {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : αβ} (h : Monotone f) :
theorem StrictMonoOn.injOn {α : Type u_1} {β : Type u_2} [LinearOrder α] [Preorder β] {f : αβ} {s : Set α} (H : StrictMonoOn f s) :
theorem StrictAntiOn.injOn {α : Type u_1} {β : Type u_2} [LinearOrder α] [Preorder β] {f : αβ} {s : Set α} (H : StrictAntiOn f s) :
theorem StrictMonoOn.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] [Preorder β] [Preorder γ] {g : βγ} {f : αβ} {s : Set α} {t : Set β} (hg : StrictMonoOn g t) (hf : StrictMonoOn f s) (hs : Set.MapsTo f s t) :
theorem StrictMonoOn.comp_strictAntiOn {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] [Preorder β] [Preorder γ] {g : βγ} {f : αβ} {s : Set α} {t : Set β} (hg : StrictMonoOn g t) (hf : StrictAntiOn f s) (hs : Set.MapsTo f s t) :
theorem StrictAntiOn.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] [Preorder β] [Preorder γ] {g : βγ} {f : αβ} {s : Set α} {t : Set β} (hg : StrictAntiOn g t) (hf : StrictAntiOn f s) (hs : Set.MapsTo f s t) :
theorem StrictAntiOn.comp_strictMonoOn {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] [Preorder β] [Preorder γ] {g : βγ} {f : αβ} {s : Set α} {t : Set β} (hg : StrictAntiOn g t) (hf : StrictMonoOn f s) (hs : Set.MapsTo f s t) :
@[simp]
theorem strictMono_restrict {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : αβ} {s : Set α} :
StrictMono (s.restrict f) StrictMonoOn f s
theorem StrictMonoOn.restrict {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : αβ} {s : Set α} :
StrictMonoOn f sStrictMono (s.restrict f)

Alias of the reverse direction of strictMono_restrict.

theorem StrictMono.of_restrict {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : αβ} {s : Set α} :
StrictMono (s.restrict f)StrictMonoOn f s

Alias of the forward direction of strictMono_restrict.

theorem StrictMono.codRestrict {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : αβ} (hf : StrictMono f) {s : Set β} (hs : ∀ (x : α), f x s) :
theorem strictMonoOn_insert_iff {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : αβ} {s : Set α} {a : α} :
StrictMonoOn f (insert a s) (∀ bs, b < af b < f a) (∀ bs, a < bf a < f b) StrictMonoOn f s
theorem strictAntiOn_insert_iff {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : αβ} {s : Set α} {a : α} :
StrictAntiOn f (insert a s) (∀ bs, b < af a < f b) (∀ bs, a < bf b < f a) StrictAntiOn f s
theorem Function.monotoneOn_of_rightInvOn_of_mapsTo {α : Type u_4} {β : Type u_5} [PartialOrder α] [LinearOrder β] {φ : βα} {ψ : αβ} {t : Set β} {s : Set α} (hφ : MonotoneOn φ t) (φψs : Set.RightInvOn ψ φ s) (ψts : Set.MapsTo ψ s t) :
theorem Function.antitoneOn_of_rightInvOn_of_mapsTo {α : Type u_1} {β : Type u_2} [PartialOrder α] [LinearOrder β] {φ : βα} {ψ : αβ} {t : Set β} {s : Set α} (hφ : AntitoneOn φ t) (φψs : Set.RightInvOn ψ φ s) (ψts : Set.MapsTo ψ s t) :