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.
• AntivaryOn 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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

@[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

@[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

theorem monovaryOn_iff_monovary {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ι → α} {g : ι → β} {s : Set ι} : MonovaryOn f g s ↔ Monovary (fun (i : ↑s) => f ↑i) fun (i : ↑s) => g ↑i

theorem antivaryOn_iff_antivary {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ι → α} {g : ι → β} {s : Set ι} : AntivaryOn f g s ↔ Antivary (fun (i : ↑s) => f ↑i) fun (i : ↑s) => g ↑i

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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)

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)

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)

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)

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

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

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

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

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

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

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

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

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)

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)

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

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

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)

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)

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

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

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

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

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

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

@[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

@[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

@[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

@[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

@[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

@[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

@[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

@[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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem StrictMono.trans_monovary {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ι → α} {g : ι → β} [PartialOrder ι] (hf : StrictMono f) (h : Monovary g f) : Monotone g

theorem StrictMono.trans_antivary {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ι → α} {g : ι → β} [PartialOrder ι] (hf : StrictMono f) (h : Antivary g f) : Antitone g

theorem StrictAnti.trans_monovary {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ι → α} {g : ι → β} [PartialOrder ι] (hf : StrictAnti f) (h : Monovary g f) : Antitone g

theorem StrictAnti.trans_antivary {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ι → α} {g : ι → β} [PartialOrder ι] (hf : StrictAnti f) (h : Antivary g f) : Monotone g

theorem StrictMonoOn.trans_monovaryOn {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ι → α} {g : ι → β} {s : Set ι} [PartialOrder ι] (hf : StrictMonoOn f s) (h : MonovaryOn g f s) : MonotoneOn g s

theorem StrictMonoOn.trans_antivaryOn {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ι → α} {g : ι → β} {s : Set ι} [PartialOrder ι] (hf : StrictMonoOn f s) (h : AntivaryOn g f s) : AntitoneOn g s

theorem StrictAntiOn.trans_monovaryOn {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ι → α} {g : ι → β} {s : Set ι} [PartialOrder ι] (hf : StrictAntiOn f s) (h : MonovaryOn g f s) : AntitoneOn g s

theorem StrictAntiOn.trans_antivaryOn {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ι → α} {g : ι → β} {s : Set ι} [PartialOrder ι] (hf : StrictAntiOn f s) (h : AntivaryOn g f s) : MonotoneOn g s

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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