# mathlib3documentation

order.monotone.monovary

# Monovariance of functions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Two functions vary together if a strict change in the first implies a change in the second.

This is in some sense a way to say that two functions f : ι → α, g : ι → β are "monotone together", without actually having an order on ι.

This condition comes up in the rearrangement inequality. See algebra.order.rearrangement.

## Main declarations #

• monovary f g: f monovaries with g. If g i < g j, then f i ≤ f j.
• antivary f g: f antivaries with g. If g i < g j, then f j ≤ f i.
• monovary_on f g s: f monovaries with g on s.
• monovary_on f g s: f antivaries with g on s.
def monovary {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] (f : ι α) (g : ι β) :
Prop

f monovaries with g if g i < g j implies f i ≤ f j.

Equations
def antivary {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] (f : ι α) (g : ι β) :
Prop

f antivaries with g if g i < g j implies f j ≤ f i.

Equations
def monovary_on {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] (f : ι α) (g : ι β) (s : set ι) :
Prop

f monovaries with g on s if g i < g j implies f i ≤ f j for all i, j ∈ s.

Equations
def antivary_on {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] (f : ι α) (g : ι β) (s : set ι) :
Prop

f antivaries with g on s if g i < g j implies f j ≤ f i for all i, j ∈ s.

Equations
@[protected]
theorem monovary.monovary_on {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] {f : ι α} {g : ι β} (h : g) (s : set ι) :
g s
@[protected]
theorem antivary.antivary_on {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] {f : ι α} {g : ι β} (h : g) (s : set ι) :
g s
@[simp]
theorem monovary_on.empty {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] {f : ι α} {g : ι β} :
g
@[simp]
theorem antivary_on.empty {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] {f : ι α} {g : ι β} :
g
@[simp]
theorem monovary_on_univ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] {f : ι α} {g : ι β} :
g
@[simp]
theorem antivary_on_univ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] {f : ι α} {g : ι β} :
g
@[protected]
theorem monovary_on.subset {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] {f : ι α} {g : ι β} {s t : set ι} (hst : s t) (h : g t) :
g s
@[protected]
theorem antivary_on.subset {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] {f : ι α} {g : ι β} {s t : set ι} (hst : s t) (h : g t) :
g s
theorem monovary_const_left {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] (g : ι β) (a : α) :
theorem antivary_const_left {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] (g : ι β) (a : α) :
theorem monovary_const_right {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] (f : ι α) (b : β) :
b)
theorem antivary_const_right {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] (f : ι α) (b : β) :
b)
theorem monovary_self {ι : Type u_1} {α : Type u_3} [preorder α] (f : ι α) :
f
theorem monovary_on_self {ι : Type u_1} {α : Type u_3} [preorder α] (f : ι α) (s : set ι) :
f s
@[protected]
theorem subsingleton.monovary {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] [subsingleton ι] (f : ι α) (g : ι β) :
g
@[protected]
theorem subsingleton.antivary {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] [subsingleton ι] (f : ι α) (g : ι β) :
g
@[protected]
theorem subsingleton.monovary_on {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] [subsingleton ι] (f : ι α) (g : ι β) (s : set ι) :
g s
@[protected]
theorem subsingleton.antivary_on {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] [subsingleton ι] (f : ι α) (g : ι β) (s : set ι) :
g s
theorem monovary_on_const_left {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] (g : ι β) (a : α) (s : set ι) :
g s
theorem antivary_on_const_left {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] (g : ι β) (a : α) (s : set ι) :
g s
theorem monovary_on_const_right {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] (f : ι α) (b : β) (s : set ι) :
b) s
theorem antivary_on_const_right {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] (f : ι α) (b : β) (s : set ι) :
b) s
theorem monovary.comp_right {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] {f : ι α} {g : ι β} (h : g) (k : ι' ι) :
monovary (f k) (g k)
theorem antivary.comp_right {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] {f : ι α} {g : ι β} (h : g) (k : ι' ι) :
antivary (f k) (g k)
theorem monovary_on.comp_right {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] {f : ι α} {g : ι β} {s : set ι} (h : g s) (k : ι' ι) :
monovary_on (f k) (g k) (k ⁻¹' s)
theorem antivary_on.comp_right {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] {f : ι α} {g : ι β} {s : set ι} (h : g s) (k : ι' ι) :
antivary_on (f k) (g k) (k ⁻¹' s)
theorem monovary.comp_monotone_left {ι : Type u_1} {α : Type u_3} {β : Type u_4} {γ : Type u_5} [preorder α] [preorder β] [preorder γ] {f : ι α} {f' : α γ} {g : ι β} (h : g) (hf : monotone f') :
monovary (f' f) g
theorem monovary.comp_antitone_left {ι : Type u_1} {α : Type u_3} {β : Type u_4} {γ : Type u_5} [preorder α] [preorder β] [preorder γ] {f : ι α} {f' : α γ} {g : ι β} (h : g) (hf : antitone f') :
antivary (f' f) g
theorem antivary.comp_monotone_left {ι : Type u_1} {α : Type u_3} {β : Type u_4} {γ : Type u_5} [preorder α] [preorder β] [preorder γ] {f : ι α} {f' : α γ} {g : ι β} (h : g) (hf : monotone f') :
antivary (f' f) g
theorem antivary.comp_antitone_left {ι : Type u_1} {α : Type u_3} {β : Type u_4} {γ : Type u_5} [preorder α] [preorder β] [preorder γ] {f : ι α} {f' : α γ} {g : ι β} (h : g) (hf : antitone f') :
monovary (f' f) g
theorem monovary_on.comp_monotone_on_left {ι : Type u_1} {α : Type u_3} {β : Type u_4} {γ : Type u_5} [preorder α] [preorder β] [preorder γ] {f : ι α} {f' : α γ} {g : ι β} {s : set ι} (h : g s) (hf : monotone f') :
monovary_on (f' f) g s
theorem monovary_on.comp_antitone_on_left {ι : Type u_1} {α : Type u_3} {β : Type u_4} {γ : Type u_5} [preorder α] [preorder β] [preorder γ] {f : ι α} {f' : α γ} {g : ι β} {s : set ι} (h : g s) (hf : antitone f') :
antivary_on (f' f) g s
theorem antivary_on.comp_monotone_on_left {ι : Type u_1} {α : Type u_3} {β : Type u_4} {γ : Type u_5} [preorder α] [preorder β] [preorder γ] {f : ι α} {f' : α γ} {g : ι β} {s : set ι} (h : g s) (hf : monotone f') :
antivary_on (f' f) g s
theorem antivary_on.comp_antitone_on_left {ι : Type u_1} {α : Type u_3} {β : Type u_4} {γ : Type u_5} [preorder α] [preorder β] [preorder γ] {f : ι α} {f' : α γ} {g : ι β} {s : set ι} (h : g s) (hf : antitone f') :
monovary_on (f' f) g s
theorem monovary.dual {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] {f : ι α} {g : ι β} :
g
theorem antivary.dual {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] {f : ι α} {g : ι β} :
g
theorem monovary.dual_left {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] {f : ι α} {g : ι β} :
g g
theorem antivary.dual_left {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] {f : ι α} {g : ι β} :
g g
theorem monovary.dual_right {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] {f : ι α} {g : ι β} :
g
theorem antivary.dual_right {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] {f : ι α} {g : ι β} :
g
theorem monovary_on.dual {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] {f : ι α} {g : ι β} {s : set ι} :
g s s
theorem antivary_on.dual {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] {f : ι α} {g : ι β} {s : set ι} :
g s s
theorem monovary_on.dual_left {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] {f : ι α} {g : ι β} {s : set ι} :
g s s
theorem antivary_on.dual_left {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] {f : ι α} {g : ι β} {s : set ι} :
g s s
theorem monovary_on.dual_right {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] {f : ι α} {g : ι β} {s : set ι} :
g s s
theorem antivary_on.dual_right {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] {f : ι α} {g : ι β} {s : set ι} :
g s s
@[simp]
theorem monovary_to_dual_left {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] {f : ι α} {g : ι β} :
g g
@[simp]
theorem monovary_to_dual_right {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] {f : ι α} {g : ι β} :
g
@[simp]
theorem antivary_to_dual_left {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] {f : ι α} {g : ι β} :
g g
@[simp]
theorem antivary_to_dual_right {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] {f : ι α} {g : ι β} :
g
@[simp]
theorem monovary_on_to_dual_left {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] {f : ι α} {g : ι β} {s : set ι} :
s g s
@[simp]
theorem monovary_on_to_dual_right {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] {f : ι α} {g : ι β} {s : set ι} :
s g s
@[simp]
theorem antivary_on_to_dual_left {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] {f : ι α} {g : ι β} {s : set ι} :
s g s
@[simp]
theorem antivary_on_to_dual_right {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] {f : ι α} {g : ι β} {s : set ι} :
s g s
@[simp]
theorem monovary_id_iff {ι : Type u_1} {α : Type u_3} [preorder α] {f : ι α}  :
@[simp]
theorem antivary_id_iff {ι : Type u_1} {α : Type u_3} [preorder α] {f : ι α}  :
@[simp]
theorem monovary_on_id_iff {ι : Type u_1} {α : Type u_3} [preorder α] {f : ι α} {s : set ι}  :
s s
@[simp]
theorem antivary_on_id_iff {ι : Type u_1} {α : Type u_3} [preorder α] {f : ι α} {s : set ι}  :
s s
@[protected]
theorem monotone.monovary {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] {f : ι α} {g : ι β} [linear_order ι] (hf : monotone f) (hg : monotone g) :
g
@[protected]
theorem monotone.antivary {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] {f : ι α} {g : ι β} [linear_order ι] (hf : monotone f) (hg : antitone g) :
g
@[protected]
theorem antitone.monovary {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] {f : ι α} {g : ι β} [linear_order ι] (hf : antitone f) (hg : antitone g) :
g
@[protected]
theorem antitone.antivary {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] {f : ι α} {g : ι β} [linear_order ι] (hf : antitone f) (hg : monotone g) :
g
@[protected]
theorem monotone_on.monovary_on {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] {f : ι α} {g : ι β} {s : set ι} [linear_order ι] (hf : s) (hg : s) :
g s
@[protected]
theorem monotone_on.antivary_on {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] {f : ι α} {g : ι β} {s : set ι} [linear_order ι] (hf : s) (hg : s) :
g s
@[protected]
theorem antitone_on.monovary_on {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] {f : ι α} {g : ι β} {s : set ι} [linear_order ι] (hf : s) (hg : s) :
g s
@[protected]
theorem antitone_on.antivary_on {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] {f : ι α} {g : ι β} {s : set ι} [linear_order ι] (hf : s) (hg : s) :
g s
theorem monovary_on.comp_monotone_on_right {ι : Type u_1} {α : Type u_3} {β : Type u_4} {γ : Type u_5} [preorder α] [linear_order β] [preorder γ] {f : ι α} {g : ι β} {g' : β γ} {s : set ι} (h : g s) (hg : (g '' s)) :
(g' g) s
theorem monovary_on.comp_antitone_on_right {ι : Type u_1} {α : Type u_3} {β : Type u_4} {γ : Type u_5} [preorder α] [linear_order β] [preorder γ] {f : ι α} {g : ι β} {g' : β γ} {s : set ι} (h : g s) (hg : (g '' s)) :
(g' g) s
theorem antivary_on.comp_monotone_on_right {ι : Type u_1} {α : Type u_3} {β : Type u_4} {γ : Type u_5} [preorder α] [linear_order β] [preorder γ] {f : ι α} {g : ι β} {g' : β γ} {s : set ι} (h : g s) (hg : (g '' s)) :
(g' g) s
theorem antivary_on.comp_antitone_on_right {ι : Type u_1} {α : Type u_3} {β : Type u_4} {γ : Type u_5} [preorder α] [linear_order β] [preorder γ] {f : ι α} {g : ι β} {g' : β γ} {s : set ι} (h : g s) (hg : (g '' s)) :
(g' g) s
@[protected]
theorem monovary.symm {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [linear_order β] {f : ι α} {g : ι β} (h : g) :
f
@[protected]
theorem antivary.symm {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [linear_order β] {f : ι α} {g : ι β} (h : g) :
f
@[protected]
theorem monovary_on.symm {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [linear_order β] {f : ι α} {g : ι β} {s : set ι} (h : g s) :
f s
@[protected]
theorem antivary_on.symm {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [linear_order β] {f : ι α} {g : ι β} {s : set ι} (h : g s) :
f s
@[protected]
theorem monovary_comm {ι : Type u_1} {α : Type u_3} {β : Type u_4} [linear_order α] [linear_order β] {f : ι α} {g : ι β} :
g f
@[protected]
theorem antivary_comm {ι : Type u_1} {α : Type u_3} {β : Type u_4} [linear_order α] [linear_order β] {f : ι α} {g : ι β} :
g f
@[protected]
theorem monovary_on_comm {ι : Type u_1} {α : Type u_3} {β : Type u_4} [linear_order α] [linear_order β] {f : ι α} {g : ι β} {s : set ι} :
g s f s
@[protected]
theorem antivary_on_comm {ι : Type u_1} {α : Type u_3} {β : Type u_4} [linear_order α] [linear_order β] {f : ι α} {g : ι β} {s : set ι} :
g s f s