Monovariance of functions #

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.
MonovaryOn f g s: f monovaries with g on s.
MonovaryOn f g s: f antivaries with g on s.

source

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

Monovary f g = ∀ ⦃i j : ι⦄, g i < g j → f i ≤ f j

Instances For

source

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

Antivary f g = ∀ ⦃i j : ι⦄, g i < g j → f j ≤ f i

Instances For

source

def MonovaryOn {ι : 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

MonovaryOn f g s = ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → g i < g j → f i ≤ f j

Instances For

source

def AntivaryOn {ι : 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

AntivaryOn f g s = ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → g i < g j → f j ≤ f i

Instances For

source

theorem Monovary.monovaryOn {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ι → α} {g : ι → β} (h : Monovary f g) (s : Set ι) :

MonovaryOn f g s

source

theorem Antivary.antivaryOn {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ι → α} {g : ι → β} (h : Antivary f g) (s : Set ι) :

AntivaryOn f g s

source

@[simp]

theorem MonovaryOn.empty {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ι → α} {g : ι → β} :

MonovaryOn f g ∅

source

@[simp]

theorem AntivaryOn.empty {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ι → α} {g : ι → β} :

AntivaryOn f g ∅

source

@[simp]

theorem monovaryOn_univ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ι → α} {g : ι → β} :

MonovaryOn f g Set.univ ↔ Monovary f g

source

@[simp]

theorem antivaryOn_univ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ι → α} {g : ι → β} :

AntivaryOn f g Set.univ ↔ Antivary f g

source

theorem MonovaryOn.subset {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ι → α} {g : ι → β} {s : Set ι} {t : Set ι} (hst : s ⊆ t) (h : MonovaryOn f g t) :

MonovaryOn f g s

source

theorem AntivaryOn.subset {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ι → α} {g : ι → β} {s : Set ι} {t : Set ι} (hst : s ⊆ t) (h : AntivaryOn f g t) :

AntivaryOn f g s

source

theorem monovary_const_left {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] (g : ι → β) (a : α) :

Monovary (Function.const ι a) g

source

theorem antivary_const_left {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] (g : ι → β) (a : α) :

Antivary (Function.const ι a) g

source

theorem monovary_const_right {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] (f : ι → α) (b : β) :

Monovary f (Function.const ι b)

source

theorem antivary_const_right {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] (f : ι → α) (b : β) :

Antivary f (Function.const ι b)

source

theorem monovary_self {ι : Type u_1} {α : Type u_3} [Preorder α] (f : ι → α) :

Monovary f f

source

theorem monovaryOn_self {ι : Type u_1} {α : Type u_3} [Preorder α] (f : ι → α) (s : Set ι) :

MonovaryOn f f s

source

theorem Subsingleton.monovary {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] [Subsingleton ι] (f : ι → α) (g : ι → β) :

Monovary f g

source

theorem Subsingleton.antivary {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] [Subsingleton ι] (f : ι → α) (g : ι → β) :

Antivary f g

source

theorem Subsingleton.monovaryOn {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] [Subsingleton ι] (f : ι → α) (g : ι → β) (s : Set ι) :

MonovaryOn f g s

source

theorem Subsingleton.antivaryOn {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] [Subsingleton ι] (f : ι → α) (g : ι → β) (s : Set ι) :

AntivaryOn f g s

source

theorem monovaryOn_const_left {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] (g : ι → β) (a : α) (s : Set ι) :

MonovaryOn (Function.const ι a) g s

source

theorem antivaryOn_const_left {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] (g : ι → β) (a : α) (s : Set ι) :

AntivaryOn (Function.const ι a) g s

source

theorem monovaryOn_const_right {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] (f : ι → α) (b : β) (s : Set ι) :

MonovaryOn f (Function.const ι b) s

source

theorem antivaryOn_const_right {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] (f : ι → α) (b : β) (s : Set ι) :

AntivaryOn f (Function.const ι b) s

source

theorem Monovary.comp_right {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ι → α} {g : ι → β} (h : Monovary f g) (k : ι' → ι) :

Monovary (f ∘ k) (g ∘ k)

source

theorem Antivary.comp_right {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ι → α} {g : ι → β} (h : Antivary f g) (k : ι' → ι) :

Antivary (f ∘ k) (g ∘ k)

source

theorem MonovaryOn.comp_right {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ι → α} {g : ι → β} {s : Set ι} (h : MonovaryOn f g s) (k : ι' → ι) :

MonovaryOn (f ∘ k) (g ∘ k) (k ⁻¹' s)

source

theorem AntivaryOn.comp_right {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ι → α} {g : ι → β} {s : Set ι} (h : AntivaryOn f g s) (k : ι' → ι) :

AntivaryOn (f ∘ k) (g ∘ k) (k ⁻¹' s)

source

theorem Monovary.comp_monotone_left {ι : Type u_1} {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Preorder α] [Preorder β] [Preorder γ] {f : ι → α} {f' : α → γ} {g : ι → β} (h : Monovary f g) (hf : Monotone f') :

Monovary (f' ∘ f) g

source

theorem Monovary.comp_antitone_left {ι : Type u_1} {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Preorder α] [Preorder β] [Preorder γ] {f : ι → α} {f' : α → γ} {g : ι → β} (h : Monovary f g) (hf : Antitone f') :

Antivary (f' ∘ f) g

source

theorem Antivary.comp_monotone_left {ι : Type u_1} {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Preorder α] [Preorder β] [Preorder γ] {f : ι → α} {f' : α → γ} {g : ι → β} (h : Antivary f g) (hf : Monotone f') :

Antivary (f' ∘ f) g

source

theorem Antivary.comp_antitone_left {ι : Type u_1} {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Preorder α] [Preorder β] [Preorder γ] {f : ι → α} {f' : α → γ} {g : ι → β} (h : Antivary f g) (hf : Antitone f') :

Monovary (f' ∘ f) g

source

theorem MonovaryOn.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 : MonovaryOn f g s) (hf : Monotone f') :

MonovaryOn (f' ∘ f) g s

source

theorem MonovaryOn.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 : MonovaryOn f g s) (hf : Antitone f') :

AntivaryOn (f' ∘ f) g s

source

theorem AntivaryOn.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 : AntivaryOn f g s) (hf : Monotone f') :

AntivaryOn (f' ∘ f) g s

source

theorem AntivaryOn.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 : AntivaryOn f g s) (hf : Antitone f') :

MonovaryOn (f' ∘ f) g s

source

theorem Monovary.dual {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ι → α} {g : ι → β} :

Monovary f g → Monovary (⇑OrderDual.toDual ∘ f) (⇑OrderDual.toDual ∘ g)

source

theorem Antivary.dual {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ι → α} {g : ι → β} :

Antivary f g → Antivary (⇑OrderDual.toDual ∘ f) (⇑OrderDual.toDual ∘ g)

source

theorem Monovary.dual_left {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ι → α} {g : ι → β} :

Monovary f g → Antivary (⇑OrderDual.toDual ∘ f) g

source

theorem Antivary.dual_left {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ι → α} {g : ι → β} :

Antivary f g → Monovary (⇑OrderDual.toDual ∘ f) g

source

theorem Monovary.dual_right {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ι → α} {g : ι → β} :

Monovary f g → Antivary f (⇑OrderDual.toDual ∘ g)

source

theorem Antivary.dual_right {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ι → α} {g : ι → β} :

Antivary f g → Monovary f (⇑OrderDual.toDual ∘ g)

source

theorem MonovaryOn.dual {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ι → α} {g : ι → β} {s : Set ι} :

MonovaryOn f g s → MonovaryOn (⇑OrderDual.toDual ∘ f) (⇑OrderDual.toDual ∘ g) s

source

theorem AntivaryOn.dual {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ι → α} {g : ι → β} {s : Set ι} :

AntivaryOn f g s → AntivaryOn (⇑OrderDual.toDual ∘ f) (⇑OrderDual.toDual ∘ g) s

source

theorem MonovaryOn.dual_left {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ι → α} {g : ι → β} {s : Set ι} :

MonovaryOn f g s → AntivaryOn (⇑OrderDual.toDual ∘ f) g s

source

theorem AntivaryOn.dual_left {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ι → α} {g : ι → β} {s : Set ι} :

AntivaryOn f g s → MonovaryOn (⇑OrderDual.toDual ∘ f) g s

source

theorem MonovaryOn.dual_right {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ι → α} {g : ι → β} {s : Set ι} :

MonovaryOn f g s → AntivaryOn f (⇑OrderDual.toDual ∘ g) s

source

theorem AntivaryOn.dual_right {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ι → α} {g : ι → β} {s : Set ι} :

AntivaryOn f g s → MonovaryOn f (⇑OrderDual.toDual ∘ g) s

source

@[simp]

theorem monovary_toDual_left {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ι → α} {g : ι → β} :

Monovary (⇑OrderDual.toDual ∘ f) g ↔ Antivary f g

source

@[simp]

theorem monovary_toDual_right {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ι → α} {g : ι → β} :

Monovary f (⇑OrderDual.toDual ∘ g) ↔ Antivary f g

source

@[simp]

theorem antivary_toDual_left {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ι → α} {g : ι → β} :

Antivary (⇑OrderDual.toDual ∘ f) g ↔ Monovary f g

source

@[simp]

theorem antivary_toDual_right {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ι → α} {g : ι → β} :

Antivary f (⇑OrderDual.toDual ∘ g) ↔ Monovary f g

source

@[simp]

theorem monovaryOn_toDual_left {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ι → α} {g : ι → β} {s : Set ι} :

MonovaryOn (⇑OrderDual.toDual ∘ f) g s ↔ AntivaryOn f g s

source

@[simp]

theorem monovaryOn_toDual_right {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ι → α} {g : ι → β} {s : Set ι} :

MonovaryOn f (⇑OrderDual.toDual ∘ g) s ↔ AntivaryOn f g s

source

@[simp]

theorem antivaryOn_toDual_left {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ι → α} {g : ι → β} {s : Set ι} :

AntivaryOn (⇑OrderDual.toDual ∘ f) g s ↔ MonovaryOn f g s

source

@[simp]

theorem antivaryOn_toDual_right {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ι → α} {g : ι → β} {s : Set ι} :

AntivaryOn f (⇑OrderDual.toDual ∘ g) s ↔ MonovaryOn f g s

source

@[simp]

theorem monovary_id_iff {ι : Type u_1} {α : Type u_3} [Preorder α] {f : ι → α} [PartialOrder ι] :

Monovary f id ↔ Monotone f

source

@[simp]

theorem antivary_id_iff {ι : Type u_1} {α : Type u_3} [Preorder α] {f : ι → α} [PartialOrder ι] :

Antivary f id ↔ Antitone f

source

@[simp]

theorem monovaryOn_id_iff {ι : Type u_1} {α : Type u_3} [Preorder α] {f : ι → α} {s : Set ι} [PartialOrder ι] :

MonovaryOn f id s ↔ MonotoneOn f s

source

@[simp]

theorem antivaryOn_id_iff {ι : Type u_1} {α : Type u_3} [Preorder α] {f : ι → α} {s : Set ι} [PartialOrder ι] :

AntivaryOn f id s ↔ AntitoneOn f s

source

theorem Monotone.monovary {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ι → α} {g : ι → β} [LinearOrder ι] (hf : Monotone f) (hg : Monotone g) :

Monovary f g

source

theorem Monotone.antivary {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ι → α} {g : ι → β} [LinearOrder ι] (hf : Monotone f) (hg : Antitone g) :

Antivary f g

source

theorem Antitone.monovary {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ι → α} {g : ι → β} [LinearOrder ι] (hf : Antitone f) (hg : Antitone g) :

Monovary f g

source

theorem Antitone.antivary {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ι → α} {g : ι → β} [LinearOrder ι] (hf : Antitone f) (hg : Monotone g) :

Antivary f g

source

theorem MonotoneOn.monovaryOn {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ι → α} {g : ι → β} {s : Set ι} [LinearOrder ι] (hf : MonotoneOn f s) (hg : MonotoneOn g s) :

MonovaryOn f g s

source

theorem MonotoneOn.antivaryOn {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ι → α} {g : ι → β} {s : Set ι} [LinearOrder ι] (hf : MonotoneOn f s) (hg : AntitoneOn g s) :

AntivaryOn f g s

source

theorem AntitoneOn.monovaryOn {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ι → α} {g : ι → β} {s : Set ι} [LinearOrder ι] (hf : AntitoneOn f s) (hg : AntitoneOn g s) :

MonovaryOn f g s

source

theorem AntitoneOn.antivaryOn {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ι → α} {g : ι → β} {s : Set ι} [LinearOrder ι] (hf : AntitoneOn f s) (hg : MonotoneOn g s) :

AntivaryOn f g s

source

theorem MonovaryOn.comp_monotoneOn_right {ι : Type u_1} {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Preorder α] [LinearOrder β] [Preorder γ] {f : ι → α} {g : ι → β} {g' : β → γ} {s : Set ι} (h : MonovaryOn f g s) (hg : MonotoneOn g' (g '' s)) :

MonovaryOn f (g' ∘ g) s

source

theorem MonovaryOn.comp_antitoneOn_right {ι : Type u_1} {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Preorder α] [LinearOrder β] [Preorder γ] {f : ι → α} {g : ι → β} {g' : β → γ} {s : Set ι} (h : MonovaryOn f g s) (hg : AntitoneOn g' (g '' s)) :

AntivaryOn f (g' ∘ g) s

source

theorem AntivaryOn.comp_monotoneOn_right {ι : Type u_1} {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Preorder α] [LinearOrder β] [Preorder γ] {f : ι → α} {g : ι → β} {g' : β → γ} {s : Set ι} (h : AntivaryOn f g s) (hg : MonotoneOn g' (g '' s)) :

AntivaryOn f (g' ∘ g) s

source

theorem AntivaryOn.comp_antitoneOn_right {ι : Type u_1} {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Preorder α] [LinearOrder β] [Preorder γ] {f : ι → α} {g : ι → β} {g' : β → γ} {s : Set ι} (h : AntivaryOn f g s) (hg : AntitoneOn g' (g '' s)) :

MonovaryOn f (g' ∘ g) s

source

theorem Monovary.symm {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [LinearOrder β] {f : ι → α} {g : ι → β} (h : Monovary f g) :

Monovary g f

source

theorem Antivary.symm {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [LinearOrder β] {f : ι → α} {g : ι → β} (h : Antivary f g) :

Antivary g f

source

theorem MonovaryOn.symm {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [LinearOrder β] {f : ι → α} {g : ι → β} {s : Set ι} (h : MonovaryOn f g s) :

MonovaryOn g f s

source

theorem AntivaryOn.symm {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [LinearOrder β] {f : ι → α} {g : ι → β} {s : Set ι} (h : AntivaryOn f g s) :

AntivaryOn g f s

source

theorem monovary_comm {ι : Type u_1} {α : Type u_3} {β : Type u_4} [LinearOrder α] [LinearOrder β] {f : ι → α} {g : ι → β} :

Monovary f g ↔ Monovary g f

source

theorem antivary_comm {ι : Type u_1} {α : Type u_3} {β : Type u_4} [LinearOrder α] [LinearOrder β] {f : ι → α} {g : ι → β} :

Antivary f g ↔ Antivary g f

source

theorem monovaryOn_comm {ι : Type u_1} {α : Type u_3} {β : Type u_4} [LinearOrder α] [LinearOrder β] {f : ι → α} {g : ι → β} {s : Set ι} :

MonovaryOn f g s ↔ MonovaryOn g f s

source

theorem antivaryOn_comm {ι : Type u_1} {α : Type u_3} {β : Type u_4} [LinearOrder α] [LinearOrder β] {f : ι → α} {g : ι → β} {s : Set ι} :

AntivaryOn f g s ↔ AntivaryOn g f s

Documentation

Mathlib.Order.Monotone.Monovary

Monovariance of functions #

Main declarations #