Monovarying functions and algebraic operations

This file characterises the interaction of ordered algebraic structures with monovariance of functions.

See also

Algebra.Order.Rearrangement for the n-ary rearrangement inequality

Algebraic operations on monovarying functions

@[simp]

theorem monovaryOn_neg_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedAddCommGroup α] [OrderedAddCommGroup β] {s : Set ι} {f : ι → α} {g : ι → β} : MonovaryOn (-f) g s ↔ AntivaryOn f g s

@[simp]

theorem monovaryOn_inv_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedCommGroup α] [OrderedCommGroup β] {s : Set ι} {f : ι → α} {g : ι → β} : MonovaryOn f⁻¹ g s ↔ AntivaryOn f g s

@[simp]

theorem antivaryOn_neg_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedAddCommGroup α] [OrderedAddCommGroup β] {s : Set ι} {f : ι → α} {g : ι → β} : AntivaryOn (-f) g s ↔ MonovaryOn f g s

@[simp]

theorem antivaryOn_inv_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedCommGroup α] [OrderedCommGroup β] {s : Set ι} {f : ι → α} {g : ι → β} : AntivaryOn f⁻¹ g s ↔ MonovaryOn f g s

@[simp]

theorem monovaryOn_neg_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedAddCommGroup α] [OrderedAddCommGroup β] {s : Set ι} {f : ι → α} {g : ι → β} : MonovaryOn f (-g) s ↔ AntivaryOn f g s

@[simp]

theorem monovaryOn_inv_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedCommGroup α] [OrderedCommGroup β] {s : Set ι} {f : ι → α} {g : ι → β} : MonovaryOn f g⁻¹ s ↔ AntivaryOn f g s

@[simp]

theorem antivaryOn_neg_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedAddCommGroup α] [OrderedAddCommGroup β] {s : Set ι} {f : ι → α} {g : ι → β} : AntivaryOn f (-g) s ↔ MonovaryOn f g s

@[simp]

theorem antivaryOn_inv_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedCommGroup α] [OrderedCommGroup β] {s : Set ι} {f : ι → α} {g : ι → β} : AntivaryOn f g⁻¹ s ↔ MonovaryOn f g s

theorem monovaryOn_neg {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedAddCommGroup α] [OrderedAddCommGroup β] {s : Set ι} {f : ι → α} {g : ι → β} : MonovaryOn (-f) (-g) s ↔ MonovaryOn f g s

theorem monovaryOn_inv {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedCommGroup α] [OrderedCommGroup β] {s : Set ι} {f : ι → α} {g : ι → β} : MonovaryOn f⁻¹ g⁻¹ s ↔ MonovaryOn f g s

theorem antivaryOn_neg {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedAddCommGroup α] [OrderedAddCommGroup β] {s : Set ι} {f : ι → α} {g : ι → β} : AntivaryOn (-f) (-g) s ↔ AntivaryOn f g s

theorem antivaryOn_inv {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedCommGroup α] [OrderedCommGroup β] {s : Set ι} {f : ι → α} {g : ι → β} : AntivaryOn f⁻¹ g⁻¹ s ↔ AntivaryOn f g s

@[simp]

theorem monovary_neg_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedAddCommGroup α] [OrderedAddCommGroup β] {f : ι → α} {g : ι → β} : Monovary (-f) g ↔ Antivary f g

@[simp]

theorem monovary_inv_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedCommGroup α] [OrderedCommGroup β] {f : ι → α} {g : ι → β} : Monovary f⁻¹ g ↔ Antivary f g

@[simp]

theorem antivary_neg_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedAddCommGroup α] [OrderedAddCommGroup β] {f : ι → α} {g : ι → β} : Antivary (-f) g ↔ Monovary f g

@[simp]

theorem antivary_inv_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedCommGroup α] [OrderedCommGroup β] {f : ι → α} {g : ι → β} : Antivary f⁻¹ g ↔ Monovary f g

@[simp]

theorem monovary_neg_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedAddCommGroup α] [OrderedAddCommGroup β] {f : ι → α} {g : ι → β} : Monovary f (-g) ↔ Antivary f g

@[simp]

theorem monovary_inv_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedCommGroup α] [OrderedCommGroup β] {f : ι → α} {g : ι → β} : Monovary f g⁻¹ ↔ Antivary f g

@[simp]

theorem antivary_neg_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedAddCommGroup α] [OrderedAddCommGroup β] {f : ι → α} {g : ι → β} : Antivary f (-g) ↔ Monovary f g

@[simp]

theorem antivary_inv_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedCommGroup α] [OrderedCommGroup β] {f : ι → α} {g : ι → β} : Antivary f g⁻¹ ↔ Monovary f g

theorem monovary_neg {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedAddCommGroup α] [OrderedAddCommGroup β] {f : ι → α} {g : ι → β} : Monovary (-f) (-g) ↔ Monovary f g

theorem monovary_inv {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedCommGroup α] [OrderedCommGroup β] {f : ι → α} {g : ι → β} : Monovary f⁻¹ g⁻¹ ↔ Monovary f g

theorem antivary_neg {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedAddCommGroup α] [OrderedAddCommGroup β] {f : ι → α} {g : ι → β} : Antivary (-f) (-g) ↔ Antivary f g

theorem antivary_inv {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedCommGroup α] [OrderedCommGroup β] {f : ι → α} {g : ι → β} : Antivary f⁻¹ g⁻¹ ↔ Antivary f g

theorem MonovaryOn.of_inv_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedCommGroup α] [OrderedCommGroup β] {s : Set ι} {f : ι → α} {g : ι → β} : MonovaryOn f⁻¹ g s → AntivaryOn f g s

Alias of the forward direction of monovaryOn_inv_left.

theorem AntivaryOn.inv_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedCommGroup α] [OrderedCommGroup β] {s : Set ι} {f : ι → α} {g : ι → β} : AntivaryOn f g s → MonovaryOn f⁻¹ g s

Alias of the reverse direction of monovaryOn_inv_left.

theorem AntivaryOn.neg_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedAddCommGroup α] [OrderedAddCommGroup β] {s : Set ι} {f : ι → α} {g : ι → β} : AntivaryOn f g s → MonovaryOn (-f) g s

theorem MonovaryOn.of_neg_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedAddCommGroup α] [OrderedAddCommGroup β] {s : Set ι} {f : ι → α} {g : ι → β} : MonovaryOn (-f) g s → AntivaryOn f g s

theorem AntivaryOn.of_inv_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedCommGroup α] [OrderedCommGroup β] {s : Set ι} {f : ι → α} {g : ι → β} : AntivaryOn f⁻¹ g s → MonovaryOn f g s

Alias of the forward direction of antivaryOn_inv_left.

theorem MonovaryOn.inv_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedCommGroup α] [OrderedCommGroup β] {s : Set ι} {f : ι → α} {g : ι → β} : MonovaryOn f g s → AntivaryOn f⁻¹ g s

Alias of the reverse direction of antivaryOn_inv_left.

theorem AntivaryOn.of_neg_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedAddCommGroup α] [OrderedAddCommGroup β] {s : Set ι} {f : ι → α} {g : ι → β} : AntivaryOn (-f) g s → MonovaryOn f g s

theorem MonovaryOn.neg_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedAddCommGroup α] [OrderedAddCommGroup β] {s : Set ι} {f : ι → α} {g : ι → β} : MonovaryOn f g s → AntivaryOn (-f) g s

theorem MonovaryOn.of_inv_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedCommGroup α] [OrderedCommGroup β] {s : Set ι} {f : ι → α} {g : ι → β} : MonovaryOn f g⁻¹ s → AntivaryOn f g s

Alias of the forward direction of monovaryOn_inv_right.

theorem AntivaryOn.inv_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedCommGroup α] [OrderedCommGroup β] {s : Set ι} {f : ι → α} {g : ι → β} : AntivaryOn f g s → MonovaryOn f g⁻¹ s

Alias of the reverse direction of monovaryOn_inv_right.

theorem AntivaryOn.neg_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedAddCommGroup α] [OrderedAddCommGroup β] {s : Set ι} {f : ι → α} {g : ι → β} : AntivaryOn f g s → MonovaryOn f (-g) s

theorem MonovaryOn.of_neg_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedAddCommGroup α] [OrderedAddCommGroup β] {s : Set ι} {f : ι → α} {g : ι → β} : MonovaryOn f (-g) s → AntivaryOn f g s

theorem AntivaryOn.of_inv_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedCommGroup α] [OrderedCommGroup β] {s : Set ι} {f : ι → α} {g : ι → β} : AntivaryOn f g⁻¹ s → MonovaryOn f g s

Alias of the forward direction of antivaryOn_inv_right.

theorem MonovaryOn.inv_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedCommGroup α] [OrderedCommGroup β] {s : Set ι} {f : ι → α} {g : ι → β} : MonovaryOn f g s → AntivaryOn f g⁻¹ s

Alias of the reverse direction of antivaryOn_inv_right.

theorem MonovaryOn.neg_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedAddCommGroup α] [OrderedAddCommGroup β] {s : Set ι} {f : ι → α} {g : ι → β} : MonovaryOn f g s → AntivaryOn f (-g) s

theorem AntivaryOn.of_neg_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedAddCommGroup α] [OrderedAddCommGroup β] {s : Set ι} {f : ι → α} {g : ι → β} : AntivaryOn f (-g) s → MonovaryOn f g s

theorem MonovaryOn.inv {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedCommGroup α] [OrderedCommGroup β] {s : Set ι} {f : ι → α} {g : ι → β} : MonovaryOn f g s → MonovaryOn f⁻¹ g⁻¹ s

Alias of the reverse direction of monovaryOn_inv.

theorem MonovaryOn.of_inv {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedCommGroup α] [OrderedCommGroup β] {s : Set ι} {f : ι → α} {g : ι → β} : MonovaryOn f⁻¹ g⁻¹ s → MonovaryOn f g s

Alias of the forward direction of monovaryOn_inv.

theorem MonovaryOn.of_neg {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedAddCommGroup α] [OrderedAddCommGroup β] {s : Set ι} {f : ι → α} {g : ι → β} : MonovaryOn (-f) (-g) s → MonovaryOn f g s

theorem MonovaryOn.neg {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedAddCommGroup α] [OrderedAddCommGroup β] {s : Set ι} {f : ι → α} {g : ι → β} : MonovaryOn f g s → MonovaryOn (-f) (-g) s

theorem AntivaryOn.inv {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedCommGroup α] [OrderedCommGroup β] {s : Set ι} {f : ι → α} {g : ι → β} : AntivaryOn f g s → AntivaryOn f⁻¹ g⁻¹ s

Alias of the reverse direction of antivaryOn_inv.

theorem AntivaryOn.of_inv {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedCommGroup α] [OrderedCommGroup β] {s : Set ι} {f : ι → α} {g : ι → β} : AntivaryOn f⁻¹ g⁻¹ s → AntivaryOn f g s

Alias of the forward direction of antivaryOn_inv.

theorem AntivaryOn.neg {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedAddCommGroup α] [OrderedAddCommGroup β] {s : Set ι} {f : ι → α} {g : ι → β} : AntivaryOn f g s → AntivaryOn (-f) (-g) s

theorem AntivaryOn.of_neg {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedAddCommGroup α] [OrderedAddCommGroup β] {s : Set ι} {f : ι → α} {g : ι → β} : AntivaryOn (-f) (-g) s → AntivaryOn f g s

theorem Monovary.of_inv_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedCommGroup α] [OrderedCommGroup β] {f : ι → α} {g : ι → β} : Monovary f⁻¹ g → Antivary f g

Alias of the forward direction of monovary_inv_left.

theorem Antivary.inv_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedCommGroup α] [OrderedCommGroup β] {f : ι → α} {g : ι → β} : Antivary f g → Monovary f⁻¹ g

Alias of the reverse direction of monovary_inv_left.

theorem Antivary.neg_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedAddCommGroup α] [OrderedAddCommGroup β] {f : ι → α} {g : ι → β} : Antivary f g → Monovary (-f) g

theorem Monovary.of_neg_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedAddCommGroup α] [OrderedAddCommGroup β] {f : ι → α} {g : ι → β} : Monovary (-f) g → Antivary f g

theorem Monovary.inv_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedCommGroup α] [OrderedCommGroup β] {f : ι → α} {g : ι → β} : Monovary f g → Antivary f⁻¹ g

Alias of the reverse direction of antivary_inv_left.

theorem Antivary.of_inv_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedCommGroup α] [OrderedCommGroup β] {f : ι → α} {g : ι → β} : Antivary f⁻¹ g → Monovary f g

Alias of the forward direction of antivary_inv_left.

theorem Monovary.neg_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedAddCommGroup α] [OrderedAddCommGroup β] {f : ι → α} {g : ι → β} : Monovary f g → Antivary (-f) g

theorem Antivary.of_neg_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedAddCommGroup α] [OrderedAddCommGroup β] {f : ι → α} {g : ι → β} : Antivary (-f) g → Monovary f g

theorem Monovary.of_inv_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedCommGroup α] [OrderedCommGroup β] {f : ι → α} {g : ι → β} : Monovary f g⁻¹ → Antivary f g

Alias of the forward direction of monovary_inv_right.

theorem Antivary.inv_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedCommGroup α] [OrderedCommGroup β] {f : ι → α} {g : ι → β} : Antivary f g → Monovary f g⁻¹

Alias of the reverse direction of monovary_inv_right.

theorem Antivary.neg_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedAddCommGroup α] [OrderedAddCommGroup β] {f : ι → α} {g : ι → β} : Antivary f g → Monovary f (-g)

theorem Monovary.of_neg_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedAddCommGroup α] [OrderedAddCommGroup β] {f : ι → α} {g : ι → β} : Monovary f (-g) → Antivary f g

theorem Monovary.inv_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedCommGroup α] [OrderedCommGroup β] {f : ι → α} {g : ι → β} : Monovary f g → Antivary f g⁻¹

Alias of the reverse direction of antivary_inv_right.

theorem Antivary.of_inv_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedCommGroup α] [OrderedCommGroup β] {f : ι → α} {g : ι → β} : Antivary f g⁻¹ → Monovary f g

Alias of the forward direction of antivary_inv_right.

theorem Antivary.of_neg_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedAddCommGroup α] [OrderedAddCommGroup β] {f : ι → α} {g : ι → β} : Antivary f (-g) → Monovary f g

theorem Monovary.neg_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedAddCommGroup α] [OrderedAddCommGroup β] {f : ι → α} {g : ι → β} : Monovary f g → Antivary f (-g)

theorem Monovary.inv {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedCommGroup α] [OrderedCommGroup β] {f : ι → α} {g : ι → β} : Monovary f g → Monovary f⁻¹ g⁻¹

Alias of the reverse direction of monovary_inv.

theorem Monovary.of_inv {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedCommGroup α] [OrderedCommGroup β] {f : ι → α} {g : ι → β} : Monovary f⁻¹ g⁻¹ → Monovary f g

Alias of the forward direction of monovary_inv.

theorem Monovary.of_neg {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedAddCommGroup α] [OrderedAddCommGroup β] {f : ι → α} {g : ι → β} : Monovary (-f) (-g) → Monovary f g

theorem Monovary.neg {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedAddCommGroup α] [OrderedAddCommGroup β] {f : ι → α} {g : ι → β} : Monovary f g → Monovary (-f) (-g)

theorem Antivary.of_inv {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedCommGroup α] [OrderedCommGroup β] {f : ι → α} {g : ι → β} : Antivary f⁻¹ g⁻¹ → Antivary f g

Alias of the forward direction of antivary_inv.

theorem Antivary.inv {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedCommGroup α] [OrderedCommGroup β] {f : ι → α} {g : ι → β} : Antivary f g → Antivary f⁻¹ g⁻¹

Alias of the reverse direction of antivary_inv.

theorem Antivary.of_neg {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedAddCommGroup α] [OrderedAddCommGroup β] {f : ι → α} {g : ι → β} : Antivary (-f) (-g) → Antivary f g

theorem Antivary.neg {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedAddCommGroup α] [OrderedAddCommGroup β] {f : ι → α} {g : ι → β} : Antivary f g → Antivary (-f) (-g)

theorem MonovaryOn.add_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedAddCommGroup α] [OrderedAddCommGroup β] {s : Set ι} {f₁ : ι → α} {f₂ : ι → α} {g : ι → β} (h₁ : MonovaryOn f₁ g s) (h₂ : MonovaryOn f₂ g s) : MonovaryOn (f₁ + f₂) g s

theorem MonovaryOn.mul_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedCommGroup α] [OrderedCommGroup β] {s : Set ι} {f₁ : ι → α} {f₂ : ι → α} {g : ι → β} (h₁ : MonovaryOn f₁ g s) (h₂ : MonovaryOn f₂ g s) : MonovaryOn (f₁ * f₂) g s

theorem AntivaryOn.add_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedAddCommGroup α] [OrderedAddCommGroup β] {s : Set ι} {f₁ : ι → α} {f₂ : ι → α} {g : ι → β} (h₁ : AntivaryOn f₁ g s) (h₂ : AntivaryOn f₂ g s) : AntivaryOn (f₁ + f₂) g s

theorem AntivaryOn.mul_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedCommGroup α] [OrderedCommGroup β] {s : Set ι} {f₁ : ι → α} {f₂ : ι → α} {g : ι → β} (h₁ : AntivaryOn f₁ g s) (h₂ : AntivaryOn f₂ g s) : AntivaryOn (f₁ * f₂) g s

theorem MonovaryOn.sub_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedAddCommGroup α] [OrderedAddCommGroup β] {s : Set ι} {f₁ : ι → α} {f₂ : ι → α} {g : ι → β} (h₁ : MonovaryOn f₁ g s) (h₂ : AntivaryOn f₂ g s) : MonovaryOn (f₁ - f₂) g s

theorem MonovaryOn.div_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedCommGroup α] [OrderedCommGroup β] {s : Set ι} {f₁ : ι → α} {f₂ : ι → α} {g : ι → β} (h₁ : MonovaryOn f₁ g s) (h₂ : AntivaryOn f₂ g s) : MonovaryOn (f₁ / f₂) g s

theorem AntivaryOn.sub_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedAddCommGroup α] [OrderedAddCommGroup β] {s : Set ι} {f₁ : ι → α} {f₂ : ι → α} {g : ι → β} (h₁ : AntivaryOn f₁ g s) (h₂ : MonovaryOn f₂ g s) : AntivaryOn (f₁ - f₂) g s

theorem AntivaryOn.div_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedCommGroup α] [OrderedCommGroup β] {s : Set ι} {f₁ : ι → α} {f₂ : ι → α} {g : ι → β} (h₁ : AntivaryOn f₁ g s) (h₂ : MonovaryOn f₂ g s) : AntivaryOn (f₁ / f₂) g s

theorem MonovaryOn.nsmul_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedAddCommGroup α] [OrderedAddCommGroup β] {s : Set ι} {f : ι → α} {g : ι → β} (hfg : MonovaryOn f g s) (n : ℕ) : MonovaryOn (n • f) g s

theorem MonovaryOn.pow_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedCommGroup α] [OrderedCommGroup β] {s : Set ι} {f : ι → α} {g : ι → β} (hfg : MonovaryOn f g s) (n : ℕ) : MonovaryOn (f ^ n) g s

theorem AntivaryOn.nsmul_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedAddCommGroup α] [OrderedAddCommGroup β] {s : Set ι} {f : ι → α} {g : ι → β} (hfg : AntivaryOn f g s) (n : ℕ) : AntivaryOn (n • f) g s

theorem AntivaryOn.pow_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedCommGroup α] [OrderedCommGroup β] {s : Set ι} {f : ι → α} {g : ι → β} (hfg : AntivaryOn f g s) (n : ℕ) : AntivaryOn (f ^ n) g s

theorem Monovary.add_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedAddCommGroup α] [OrderedAddCommGroup β] {f₁ : ι → α} {f₂ : ι → α} {g : ι → β} (h₁ : Monovary f₁ g) (h₂ : Monovary f₂ g) : Monovary (f₁ + f₂) g

theorem Monovary.mul_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedCommGroup α] [OrderedCommGroup β] {f₁ : ι → α} {f₂ : ι → α} {g : ι → β} (h₁ : Monovary f₁ g) (h₂ : Monovary f₂ g) : Monovary (f₁ * f₂) g

theorem Antivary.add_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedAddCommGroup α] [OrderedAddCommGroup β] {f₁ : ι → α} {f₂ : ι → α} {g : ι → β} (h₁ : Antivary f₁ g) (h₂ : Antivary f₂ g) : Antivary (f₁ + f₂) g

theorem Antivary.mul_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedCommGroup α] [OrderedCommGroup β] {f₁ : ι → α} {f₂ : ι → α} {g : ι → β} (h₁ : Antivary f₁ g) (h₂ : Antivary f₂ g) : Antivary (f₁ * f₂) g

theorem Monovary.sub_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedAddCommGroup α] [OrderedAddCommGroup β] {f₁ : ι → α} {f₂ : ι → α} {g : ι → β} (h₁ : Monovary f₁ g) (h₂ : Antivary f₂ g) : Monovary (f₁ - f₂) g

theorem Monovary.div_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedCommGroup α] [OrderedCommGroup β] {f₁ : ι → α} {f₂ : ι → α} {g : ι → β} (h₁ : Monovary f₁ g) (h₂ : Antivary f₂ g) : Monovary (f₁ / f₂) g

theorem Antivary.sub_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedAddCommGroup α] [OrderedAddCommGroup β] {f₁ : ι → α} {f₂ : ι → α} {g : ι → β} (h₁ : Antivary f₁ g) (h₂ : Monovary f₂ g) : Antivary (f₁ - f₂) g

theorem Antivary.div_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedCommGroup α] [OrderedCommGroup β] {f₁ : ι → α} {f₂ : ι → α} {g : ι → β} (h₁ : Antivary f₁ g) (h₂ : Monovary f₂ g) : Antivary (f₁ / f₂) g

theorem Monovary.nsmul_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedAddCommGroup α] [OrderedAddCommGroup β] {f : ι → α} {g : ι → β} (hfg : Monovary f g) (n : ℕ) : Monovary (n • f) g

theorem Monovary.pow_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedCommGroup α] [OrderedCommGroup β] {f : ι → α} {g : ι → β} (hfg : Monovary f g) (n : ℕ) : Monovary (f ^ n) g

theorem Antivary.nsmul_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedAddCommGroup α] [OrderedAddCommGroup β] {f : ι → α} {g : ι → β} (hfg : Antivary f g) (n : ℕ) : Antivary (n • f) g

theorem Antivary.pow_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedCommGroup α] [OrderedCommGroup β] {f : ι → α} {g : ι → β} (hfg : Antivary f g) (n : ℕ) : Antivary (f ^ n) g

theorem MonovaryOn.add_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedAddCommGroup α] [LinearOrderedAddCommGroup β] {s : Set ι} {f : ι → α} {g₁ : ι → β} {g₂ : ι → β} (h₁ : MonovaryOn f g₁ s) (h₂ : MonovaryOn f g₂ s) : MonovaryOn f (g₁ + g₂) s

theorem MonovaryOn.mul_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedCommGroup α] [LinearOrderedCommGroup β] {s : Set ι} {f : ι → α} {g₁ : ι → β} {g₂ : ι → β} (h₁ : MonovaryOn f g₁ s) (h₂ : MonovaryOn f g₂ s) : MonovaryOn f (g₁ * g₂) s

theorem AntivaryOn.add_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedAddCommGroup α] [LinearOrderedAddCommGroup β] {s : Set ι} {f : ι → α} {g₁ : ι → β} {g₂ : ι → β} (h₁ : AntivaryOn f g₁ s) (h₂ : AntivaryOn f g₂ s) : AntivaryOn f (g₁ + g₂) s

theorem AntivaryOn.mul_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedCommGroup α] [LinearOrderedCommGroup β] {s : Set ι} {f : ι → α} {g₁ : ι → β} {g₂ : ι → β} (h₁ : AntivaryOn f g₁ s) (h₂ : AntivaryOn f g₂ s) : AntivaryOn f (g₁ * g₂) s

theorem MonovaryOn.sub_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedAddCommGroup α] [LinearOrderedAddCommGroup β] {s : Set ι} {f : ι → α} {g₁ : ι → β} {g₂ : ι → β} (h₁ : MonovaryOn f g₁ s) (h₂ : AntivaryOn f g₂ s) : MonovaryOn f (g₁ - g₂) s

theorem MonovaryOn.div_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedCommGroup α] [LinearOrderedCommGroup β] {s : Set ι} {f : ι → α} {g₁ : ι → β} {g₂ : ι → β} (h₁ : MonovaryOn f g₁ s) (h₂ : AntivaryOn f g₂ s) : MonovaryOn f (g₁ / g₂) s

theorem AntivaryOn.sub_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedAddCommGroup α] [LinearOrderedAddCommGroup β] {s : Set ι} {f : ι → α} {g₁ : ι → β} {g₂ : ι → β} (h₁ : AntivaryOn f g₁ s) (h₂ : MonovaryOn f g₂ s) : AntivaryOn f (g₁ - g₂) s

theorem AntivaryOn.div_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedCommGroup α] [LinearOrderedCommGroup β] {s : Set ι} {f : ι → α} {g₁ : ι → β} {g₂ : ι → β} (h₁ : AntivaryOn f g₁ s) (h₂ : MonovaryOn f g₂ s) : AntivaryOn f (g₁ / g₂) s

theorem MonovaryOn.nsmul_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedAddCommGroup α] [LinearOrderedAddCommGroup β] {s : Set ι} {f : ι → α} {g : ι → β} (hfg : MonovaryOn f g s) (n : ℕ) : MonovaryOn f (n • g) s

theorem MonovaryOn.pow_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedCommGroup α] [LinearOrderedCommGroup β] {s : Set ι} {f : ι → α} {g : ι → β} (hfg : MonovaryOn f g s) (n : ℕ) : MonovaryOn f (g ^ n) s

theorem AntivaryOn.nsmul_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedAddCommGroup α] [LinearOrderedAddCommGroup β] {s : Set ι} {f : ι → α} {g : ι → β} (hfg : AntivaryOn f g s) (n : ℕ) : AntivaryOn f (n • g) s

theorem AntivaryOn.pow_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedCommGroup α] [LinearOrderedCommGroup β] {s : Set ι} {f : ι → α} {g : ι → β} (hfg : AntivaryOn f g s) (n : ℕ) : AntivaryOn f (g ^ n) s

theorem Monovary.add_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedAddCommGroup α] [LinearOrderedAddCommGroup β] {f : ι → α} {g₁ : ι → β} {g₂ : ι → β} (h₁ : Monovary f g₁) (h₂ : Monovary f g₂) : Monovary f (g₁ + g₂)

theorem Monovary.mul_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedCommGroup α] [LinearOrderedCommGroup β] {f : ι → α} {g₁ : ι → β} {g₂ : ι → β} (h₁ : Monovary f g₁) (h₂ : Monovary f g₂) : Monovary f (g₁ * g₂)

theorem Antivary.add_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedAddCommGroup α] [LinearOrderedAddCommGroup β] {f : ι → α} {g₁ : ι → β} {g₂ : ι → β} (h₁ : Antivary f g₁) (h₂ : Antivary f g₂) : Antivary f (g₁ + g₂)

theorem Antivary.mul_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedCommGroup α] [LinearOrderedCommGroup β] {f : ι → α} {g₁ : ι → β} {g₂ : ι → β} (h₁ : Antivary f g₁) (h₂ : Antivary f g₂) : Antivary f (g₁ * g₂)

theorem Monovary.sub_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedAddCommGroup α] [LinearOrderedAddCommGroup β] {f : ι → α} {g₁ : ι → β} {g₂ : ι → β} (h₁ : Monovary f g₁) (h₂ : Antivary f g₂) : Monovary f (g₁ - g₂)

theorem Monovary.div_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedCommGroup α] [LinearOrderedCommGroup β] {f : ι → α} {g₁ : ι → β} {g₂ : ι → β} (h₁ : Monovary f g₁) (h₂ : Antivary f g₂) : Monovary f (g₁ / g₂)

theorem Antivary.sub_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedAddCommGroup α] [LinearOrderedAddCommGroup β] {f : ι → α} {g₁ : ι → β} {g₂ : ι → β} (h₁ : Antivary f g₁) (h₂ : Monovary f g₂) : Antivary f (g₁ - g₂)

theorem Antivary.div_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedCommGroup α] [LinearOrderedCommGroup β] {f : ι → α} {g₁ : ι → β} {g₂ : ι → β} (h₁ : Antivary f g₁) (h₂ : Monovary f g₂) : Antivary f (g₁ / g₂)

theorem Monovary.nsmul_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedAddCommGroup α] [LinearOrderedAddCommGroup β] {f : ι → α} {g : ι → β} (hfg : Monovary f g) (n : ℕ) : Monovary f (n • g)

theorem Monovary.pow_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedCommGroup α] [LinearOrderedCommGroup β] {f : ι → α} {g : ι → β} (hfg : Monovary f g) (n : ℕ) : Monovary f (g ^ n)

theorem Antivary.nsmul_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedAddCommGroup α] [LinearOrderedAddCommGroup β] {f : ι → α} {g : ι → β} (hfg : Antivary f g) (n : ℕ) : Antivary f (n • g)

theorem Antivary.pow_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedCommGroup α] [LinearOrderedCommGroup β] {f : ι → α} {g : ι → β} (hfg : Antivary f g) (n : ℕ) : Antivary f (g ^ n)

theorem MonovaryOn.mul_left₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedSemiring α] [OrderedSemiring β] {s : Set ι} {f₁ : ι → α} {f₂ : ι → α} {g : ι → β} (hf₁ : ∀ i ∈ s, 0 ≤ f₁ i) (hf₂ : ∀ i ∈ s, 0 ≤ f₂ i) (h₁ : MonovaryOn f₁ g s) (h₂ : MonovaryOn f₂ g s) : MonovaryOn (f₁ * f₂) g s

theorem AntivaryOn.mul_left₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedSemiring α] [OrderedSemiring β] {s : Set ι} {f₁ : ι → α} {f₂ : ι → α} {g : ι → β} (hf₁ : ∀ i ∈ s, 0 ≤ f₁ i) (hf₂ : ∀ i ∈ s, 0 ≤ f₂ i) (h₁ : AntivaryOn f₁ g s) (h₂ : AntivaryOn f₂ g s) : AntivaryOn (f₁ * f₂) g s

theorem MonovaryOn.pow_left₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedSemiring α] [OrderedSemiring β] {s : Set ι} {f : ι → α} {g : ι → β} (hf : ∀ i ∈ s, 0 ≤ f i) (hfg : MonovaryOn f g s) (n : ℕ) : MonovaryOn (f ^ n) g s

theorem AntivaryOn.pow_left₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedSemiring α] [OrderedSemiring β] {s : Set ι} {f : ι → α} {g : ι → β} (hf : ∀ i ∈ s, 0 ≤ f i) (hfg : AntivaryOn f g s) (n : ℕ) : AntivaryOn (f ^ n) g s

theorem Monovary.mul_left₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedSemiring α] [OrderedSemiring β] {f₁ : ι → α} {f₂ : ι → α} {g : ι → β} (hf₁ : 0 ≤ f₁) (hf₂ : 0 ≤ f₂) (h₁ : Monovary f₁ g) (h₂ : Monovary f₂ g) : Monovary (f₁ * f₂) g

theorem Antivary.mul_left₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedSemiring α] [OrderedSemiring β] {f₁ : ι → α} {f₂ : ι → α} {g : ι → β} (hf₁ : 0 ≤ f₁) (hf₂ : 0 ≤ f₂) (h₁ : Antivary f₁ g) (h₂ : Antivary f₂ g) : Antivary (f₁ * f₂) g

theorem Monovary.pow_left₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedSemiring α] [OrderedSemiring β] {f : ι → α} {g : ι → β} (hf : 0 ≤ f) (hfg : Monovary f g) (n : ℕ) : Monovary (f ^ n) g

theorem Antivary.pow_left₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedSemiring α] [OrderedSemiring β] {f : ι → α} {g : ι → β} (hf : 0 ≤ f) (hfg : Antivary f g) (n : ℕ) : Antivary (f ^ n) g

theorem MonovaryOn.mul_right₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedSemiring α] [LinearOrderedSemiring β] {s : Set ι} {f : ι → α} {g₁ : ι → β} {g₂ : ι → β} (hg₁ : ∀ i ∈ s, 0 ≤ g₁ i) (hg₂ : ∀ i ∈ s, 0 ≤ g₂ i) (h₁ : MonovaryOn f g₁ s) (h₂ : MonovaryOn f g₂ s) : MonovaryOn f (g₁ * g₂) s

theorem AntivaryOn.mul_right₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedSemiring α] [LinearOrderedSemiring β] {s : Set ι} {f : ι → α} {g₁ : ι → β} {g₂ : ι → β} (hg₁ : ∀ i ∈ s, 0 ≤ g₁ i) (hg₂ : ∀ i ∈ s, 0 ≤ g₂ i) (h₁ : AntivaryOn f g₁ s) (h₂ : AntivaryOn f g₂ s) : AntivaryOn f (g₁ * g₂) s

theorem MonovaryOn.pow_right₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedSemiring α] [LinearOrderedSemiring β] {s : Set ι} {f : ι → α} {g : ι → β} (hg : ∀ i ∈ s, 0 ≤ g i) (hfg : MonovaryOn f g s) (n : ℕ) : MonovaryOn f (g ^ n) s

theorem AntivaryOn.pow_right₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedSemiring α] [LinearOrderedSemiring β] {s : Set ι} {f : ι → α} {g : ι → β} (hg : ∀ i ∈ s, 0 ≤ g i) (hfg : AntivaryOn f g s) (n : ℕ) : AntivaryOn f (g ^ n) s

theorem Monovary.mul_right₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedSemiring α] [LinearOrderedSemiring β] {f : ι → α} {g₁ : ι → β} {g₂ : ι → β} (hg₁ : 0 ≤ g₁) (hg₂ : 0 ≤ g₂) (h₁ : Monovary f g₁) (h₂ : Monovary f g₂) : Monovary f (g₁ * g₂)

theorem Antivary.mul_right₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedSemiring α] [LinearOrderedSemiring β] {f : ι → α} {g₁ : ι → β} {g₂ : ι → β} (hg₁ : 0 ≤ g₁) (hg₂ : 0 ≤ g₂) (h₁ : Antivary f g₁) (h₂ : Antivary f g₂) : Antivary f (g₁ * g₂)

theorem Monovary.pow_right₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedSemiring α] [LinearOrderedSemiring β] {f : ι → α} {g : ι → β} (hg : 0 ≤ g) (hfg : Monovary f g) (n : ℕ) : Monovary f (g ^ n)

theorem Antivary.pow_right₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedSemiring α] [LinearOrderedSemiring β] {f : ι → α} {g : ι → β} (hg : 0 ≤ g) (hfg : Antivary f g) (n : ℕ) : Antivary f (g ^ n)

@[simp]

theorem monovaryOn_inv_left₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedSemifield α] [LinearOrderedSemifield β] {s : Set ι} {f : ι → α} {g : ι → β} (hf : ∀ i ∈ s, 0 < f i) : MonovaryOn f⁻¹ g s ↔ AntivaryOn f g s

@[simp]

theorem antivaryOn_inv_left₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedSemifield α] [LinearOrderedSemifield β] {s : Set ι} {f : ι → α} {g : ι → β} (hf : ∀ i ∈ s, 0 < f i) : AntivaryOn f⁻¹ g s ↔ MonovaryOn f g s

@[simp]

theorem monovaryOn_inv_right₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedSemifield α] [LinearOrderedSemifield β] {s : Set ι} {f : ι → α} {g : ι → β} (hg : ∀ i ∈ s, 0 < g i) : MonovaryOn f g⁻¹ s ↔ AntivaryOn f g s

@[simp]

theorem antivaryOn_inv_right₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedSemifield α] [LinearOrderedSemifield β] {s : Set ι} {f : ι → α} {g : ι → β} (hg : ∀ i ∈ s, 0 < g i) : AntivaryOn f g⁻¹ s ↔ MonovaryOn f g s

theorem monovaryOn_inv₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedSemifield α] [LinearOrderedSemifield β] {s : Set ι} {f : ι → α} {g : ι → β} (hf : ∀ i ∈ s, 0 < f i) (hg : ∀ i ∈ s, 0 < g i) : MonovaryOn f⁻¹ g⁻¹ s ↔ MonovaryOn f g s

theorem antivaryOn_inv₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedSemifield α] [LinearOrderedSemifield β] {s : Set ι} {f : ι → α} {g : ι → β} (hf : ∀ i ∈ s, 0 < f i) (hg : ∀ i ∈ s, 0 < g i) : AntivaryOn f⁻¹ g⁻¹ s ↔ AntivaryOn f g s

@[simp]

theorem monovary_inv_left₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedSemifield α] [LinearOrderedSemifield β] {f : ι → α} {g : ι → β} (hf : StrongLT 0 f) : Monovary f⁻¹ g ↔ Antivary f g

@[simp]

theorem antivary_inv_left₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedSemifield α] [LinearOrderedSemifield β] {f : ι → α} {g : ι → β} (hf : StrongLT 0 f) : Antivary f⁻¹ g ↔ Monovary f g

@[simp]

theorem monovary_inv_right₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedSemifield α] [LinearOrderedSemifield β] {f : ι → α} {g : ι → β} (hg : StrongLT 0 g) : Monovary f g⁻¹ ↔ Antivary f g

@[simp]

theorem antivary_inv_right₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedSemifield α] [LinearOrderedSemifield β] {f : ι → α} {g : ι → β} (hg : StrongLT 0 g) : Antivary f g⁻¹ ↔ Monovary f g

theorem monovary_inv₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedSemifield α] [LinearOrderedSemifield β] {f : ι → α} {g : ι → β} (hf : StrongLT 0 f) (hg : StrongLT 0 g) : Monovary f⁻¹ g⁻¹ ↔ Monovary f g

theorem antivary_inv₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedSemifield α] [LinearOrderedSemifield β] {f : ι → α} {g : ι → β} (hf : StrongLT 0 f) (hg : StrongLT 0 g) : Antivary f⁻¹ g⁻¹ ↔ Antivary f g

theorem MonovaryOn.of_inv_left₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedSemifield α] [LinearOrderedSemifield β] {s : Set ι} {f : ι → α} {g : ι → β} (hf : ∀ i ∈ s, 0 < f i) : MonovaryOn f⁻¹ g s → AntivaryOn f g s

Alias of the forward direction of monovaryOn_inv_left₀.

theorem AntivaryOn.inv_left₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedSemifield α] [LinearOrderedSemifield β] {s : Set ι} {f : ι → α} {g : ι → β} (hf : ∀ i ∈ s, 0 < f i) : AntivaryOn f g s → MonovaryOn f⁻¹ g s

Alias of the reverse direction of monovaryOn_inv_left₀.

theorem MonovaryOn.inv_left₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedSemifield α] [LinearOrderedSemifield β] {s : Set ι} {f : ι → α} {g : ι → β} (hf : ∀ i ∈ s, 0 < f i) : MonovaryOn f g s → AntivaryOn f⁻¹ g s

Alias of the reverse direction of antivaryOn_inv_left₀.

theorem AntivaryOn.of_inv_left₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedSemifield α] [LinearOrderedSemifield β] {s : Set ι} {f : ι → α} {g : ι → β} (hf : ∀ i ∈ s, 0 < f i) : AntivaryOn f⁻¹ g s → MonovaryOn f g s

Alias of the forward direction of antivaryOn_inv_left₀.

theorem AntivaryOn.inv_right₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedSemifield α] [LinearOrderedSemifield β] {s : Set ι} {f : ι → α} {g : ι → β} (hg : ∀ i ∈ s, 0 < g i) : AntivaryOn f g s → MonovaryOn f g⁻¹ s

Alias of the reverse direction of monovaryOn_inv_right₀.

theorem MonovaryOn.of_inv_right₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedSemifield α] [LinearOrderedSemifield β] {s : Set ι} {f : ι → α} {g : ι → β} (hg : ∀ i ∈ s, 0 < g i) : MonovaryOn f g⁻¹ s → AntivaryOn f g s

Alias of the forward direction of monovaryOn_inv_right₀.

theorem AntivaryOn.of_inv_right₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedSemifield α] [LinearOrderedSemifield β] {s : Set ι} {f : ι → α} {g : ι → β} (hg : ∀ i ∈ s, 0 < g i) : AntivaryOn f g⁻¹ s → MonovaryOn f g s

Alias of the forward direction of antivaryOn_inv_right₀.

theorem MonovaryOn.inv_right₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedSemifield α] [LinearOrderedSemifield β] {s : Set ι} {f : ι → α} {g : ι → β} (hg : ∀ i ∈ s, 0 < g i) : MonovaryOn f g s → AntivaryOn f g⁻¹ s

Alias of the reverse direction of antivaryOn_inv_right₀.

theorem MonovaryOn.of_inv₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedSemifield α] [LinearOrderedSemifield β] {s : Set ι} {f : ι → α} {g : ι → β} (hf : ∀ i ∈ s, 0 < f i) (hg : ∀ i ∈ s, 0 < g i) : MonovaryOn f⁻¹ g⁻¹ s → MonovaryOn f g s

Alias of the forward direction of monovaryOn_inv₀.

theorem MonovaryOn.inv₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedSemifield α] [LinearOrderedSemifield β] {s : Set ι} {f : ι → α} {g : ι → β} (hf : ∀ i ∈ s, 0 < f i) (hg : ∀ i ∈ s, 0 < g i) : MonovaryOn f g s → MonovaryOn f⁻¹ g⁻¹ s

Alias of the reverse direction of monovaryOn_inv₀.

theorem AntivaryOn.of_inv₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedSemifield α] [LinearOrderedSemifield β] {s : Set ι} {f : ι → α} {g : ι → β} (hf : ∀ i ∈ s, 0 < f i) (hg : ∀ i ∈ s, 0 < g i) : AntivaryOn f⁻¹ g⁻¹ s → AntivaryOn f g s

Alias of the forward direction of antivaryOn_inv₀.

theorem AntivaryOn.inv₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedSemifield α] [LinearOrderedSemifield β] {s : Set ι} {f : ι → α} {g : ι → β} (hf : ∀ i ∈ s, 0 < f i) (hg : ∀ i ∈ s, 0 < g i) : AntivaryOn f g s → AntivaryOn f⁻¹ g⁻¹ s

Alias of the reverse direction of antivaryOn_inv₀.

theorem Monovary.of_inv_left₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedSemifield α] [LinearOrderedSemifield β] {f : ι → α} {g : ι → β} (hf : StrongLT 0 f) : Monovary f⁻¹ g → Antivary f g

Alias of the forward direction of monovary_inv_left₀.

theorem Antivary.inv_left₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedSemifield α] [LinearOrderedSemifield β] {f : ι → α} {g : ι → β} (hf : StrongLT 0 f) : Antivary f g → Monovary f⁻¹ g

Alias of the reverse direction of monovary_inv_left₀.

theorem Monovary.inv_left₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedSemifield α] [LinearOrderedSemifield β] {f : ι → α} {g : ι → β} (hf : StrongLT 0 f) : Monovary f g → Antivary f⁻¹ g

Alias of the reverse direction of antivary_inv_left₀.

theorem Antivary.of_inv_left₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedSemifield α] [LinearOrderedSemifield β] {f : ι → α} {g : ι → β} (hf : StrongLT 0 f) : Antivary f⁻¹ g → Monovary f g

Alias of the forward direction of antivary_inv_left₀.

theorem Monovary.of_inv_right₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedSemifield α] [LinearOrderedSemifield β] {f : ι → α} {g : ι → β} (hg : StrongLT 0 g) : Monovary f g⁻¹ → Antivary f g

Alias of the forward direction of monovary_inv_right₀.

theorem Antivary.inv_right₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedSemifield α] [LinearOrderedSemifield β] {f : ι → α} {g : ι → β} (hg : StrongLT 0 g) : Antivary f g → Monovary f g⁻¹

Alias of the reverse direction of monovary_inv_right₀.

theorem Antivary.of_inv_right₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedSemifield α] [LinearOrderedSemifield β] {f : ι → α} {g : ι → β} (hg : StrongLT 0 g) : Antivary f g⁻¹ → Monovary f g

Alias of the forward direction of antivary_inv_right₀.

theorem Monovary.inv_right₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedSemifield α] [LinearOrderedSemifield β] {f : ι → α} {g : ι → β} (hg : StrongLT 0 g) : Monovary f g → Antivary f g⁻¹

Alias of the reverse direction of antivary_inv_right₀.

theorem Monovary.inv₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedSemifield α] [LinearOrderedSemifield β] {f : ι → α} {g : ι → β} (hf : StrongLT 0 f) (hg : StrongLT 0 g) : Monovary f g → Monovary f⁻¹ g⁻¹

Alias of the reverse direction of monovary_inv₀.

theorem Monovary.of_inv₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedSemifield α] [LinearOrderedSemifield β] {f : ι → α} {g : ι → β} (hf : StrongLT 0 f) (hg : StrongLT 0 g) : Monovary f⁻¹ g⁻¹ → Monovary f g

Alias of the forward direction of monovary_inv₀.

theorem Antivary.inv₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedSemifield α] [LinearOrderedSemifield β] {f : ι → α} {g : ι → β} (hf : StrongLT 0 f) (hg : StrongLT 0 g) : Antivary f g → Antivary f⁻¹ g⁻¹

Alias of the reverse direction of antivary_inv₀.

theorem Antivary.of_inv₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedSemifield α] [LinearOrderedSemifield β] {f : ι → α} {g : ι → β} (hf : StrongLT 0 f) (hg : StrongLT 0 g) : Antivary f⁻¹ g⁻¹ → Antivary f g

Alias of the forward direction of antivary_inv₀.

theorem MonovaryOn.div_left₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedSemifield α] [LinearOrderedSemifield β] {s : Set ι} {f₁ : ι → α} {f₂ : ι → α} {g : ι → β} (hf₁ : ∀ i ∈ s, 0 ≤ f₁ i) (hf₂ : ∀ i ∈ s, 0 < f₂ i) (h₁ : MonovaryOn f₁ g s) (h₂ : AntivaryOn f₂ g s) : MonovaryOn (f₁ / f₂) g s

theorem AntivaryOn.div_left₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedSemifield α] [LinearOrderedSemifield β] {s : Set ι} {f₁ : ι → α} {f₂ : ι → α} {g : ι → β} (hf₁ : ∀ i ∈ s, 0 ≤ f₁ i) (hf₂ : ∀ i ∈ s, 0 < f₂ i) (h₁ : AntivaryOn f₁ g s) (h₂ : MonovaryOn f₂ g s) : AntivaryOn (f₁ / f₂) g s

theorem Monovary.div_left₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedSemifield α] [LinearOrderedSemifield β] {f₁ : ι → α} {f₂ : ι → α} {g : ι → β} (hf₁ : 0 ≤ f₁) (hf₂ : StrongLT 0 f₂) (h₁ : Monovary f₁ g) (h₂ : Antivary f₂ g) : Monovary (f₁ / f₂) g

theorem Antivary.div_left₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedSemifield α] [LinearOrderedSemifield β] {f₁ : ι → α} {f₂ : ι → α} {g : ι → β} (hf₁ : 0 ≤ f₁) (hf₂ : StrongLT 0 f₂) (h₁ : Antivary f₁ g) (h₂ : Monovary f₂ g) : Antivary (f₁ / f₂) g

theorem MonovaryOn.div_right₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedSemifield α] [LinearOrderedSemifield β] {s : Set ι} {f : ι → α} {g₁ : ι → β} {g₂ : ι → β} (hg₁ : ∀ i ∈ s, 0 ≤ g₁ i) (hg₂ : ∀ i ∈ s, 0 < g₂ i) (h₁ : MonovaryOn f g₁ s) (h₂ : AntivaryOn f g₂ s) : MonovaryOn f (g₁ / g₂) s

theorem AntivaryOn.div_right₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedSemifield α] [LinearOrderedSemifield β] {s : Set ι} {f : ι → α} {g₁ : ι → β} {g₂ : ι → β} (hg₁ : ∀ i ∈ s, 0 ≤ g₁ i) (hg₂ : ∀ i ∈ s, 0 < g₂ i) (h₁ : AntivaryOn f g₁ s) (h₂ : MonovaryOn f g₂ s) : AntivaryOn f (g₁ / g₂) s

theorem Monovary.div_right₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedSemifield α] [LinearOrderedSemifield β] {f : ι → α} {g₁ : ι → β} {g₂ : ι → β} (hg₁ : 0 ≤ g₁) (hg₂ : StrongLT 0 g₂) (h₁ : Monovary f g₁) (h₂ : Antivary f g₂) : Monovary f (g₁ / g₂)

theorem Antivary.div_right₀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedSemifield α] [LinearOrderedSemifield β] {f : ι → α} {g₁ : ι → β} {g₂ : ι → β} (hg₁ : 0 ≤ g₁) (hg₂ : StrongLT 0 g₂) (h₁ : Antivary f g₁) (h₂ : Monovary f g₂) : Antivary f (g₁ / g₂)

Rearrangement inequality characterisation

theorem monovaryOn_iff_forall_smul_nonneg {ι : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedRing α] [LinearOrderedAddCommGroup β] [Module α β] [OrderedSMul α β] {f : ι → α} {g : ι → β} {s : Set ι} : MonovaryOn f g s ↔ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → 0 ≤ (f j - f i) • (g j - g i)

theorem antivaryOn_iff_forall_smul_nonpos {ι : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedRing α] [LinearOrderedAddCommGroup β] [Module α β] [OrderedSMul α β] {f : ι → α} {g : ι → β} {s : Set ι} : AntivaryOn f g s ↔ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → (f j - f i) • (g j - g i) ≤ 0

theorem monovary_iff_forall_smul_nonneg {ι : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedRing α] [LinearOrderedAddCommGroup β] [Module α β] [OrderedSMul α β] {f : ι → α} {g : ι → β} : Monovary f g ↔ ∀ (i j : ι), 0 ≤ (f j - f i) • (g j - g i)

theorem antivary_iff_forall_smul_nonpos {ι : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedRing α] [LinearOrderedAddCommGroup β] [Module α β] [OrderedSMul α β] {f : ι → α} {g : ι → β} : Antivary f g ↔ ∀ (i j : ι), (f j - f i) • (g j - g i) ≤ 0

theorem monovaryOn_iff_smul_rearrangement {ι : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedRing α] [LinearOrderedAddCommGroup β] [Module α β] [OrderedSMul α β] {f : ι → α} {g : ι → β} {s : Set ι} : MonovaryOn f g s ↔ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → f i • g j + f j • g i ≤ f i • g i + f j • g j

Two functions monovary iff the rearrangement inequality holds.

theorem antivaryOn_iff_smul_rearrangement {ι : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedRing α] [LinearOrderedAddCommGroup β] [Module α β] [OrderedSMul α β] {f : ι → α} {g : ι → β} {s : Set ι} : AntivaryOn f g s ↔ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → f i • g i + f j • g j ≤ f i • g j + f j • g i

Two functions antivary iff the rearrangement inequality holds.

theorem monovary_iff_smul_rearrangement {ι : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedRing α] [LinearOrderedAddCommGroup β] [Module α β] [OrderedSMul α β] {f : ι → α} {g : ι → β} : Monovary f g ↔ ∀ (i j : ι), f i • g j + f j • g i ≤ f i • g i + f j • g j

Two functions monovary iff the rearrangement inequality holds.

theorem antivary_iff_smul_rearrangement {ι : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedRing α] [LinearOrderedAddCommGroup β] [Module α β] [OrderedSMul α β] {f : ι → α} {g : ι → β} : Antivary f g ↔ ∀ (i j : ι), f i • g i + f j • g j ≤ f i • g j + f j • g i

Two functions antivary iff the rearrangement inequality holds.

theorem MonovaryOn.sub_smul_sub_nonneg {ι : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedRing α] [LinearOrderedAddCommGroup β] [Module α β] [OrderedSMul α β] {f : ι → α} {g : ι → β} {s : Set ι} : MonovaryOn f g s → ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → 0 ≤ (f j - f i) • (g j - g i)

Alias of the forward direction of monovaryOn_iff_forall_smul_nonneg.

theorem AntivaryOn.sub_smul_sub_nonpos {ι : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedRing α] [LinearOrderedAddCommGroup β] [Module α β] [OrderedSMul α β] {f : ι → α} {g : ι → β} {s : Set ι} : AntivaryOn f g s → ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → (f j - f i) • (g j - g i) ≤ 0

Alias of the forward direction of antivaryOn_iff_forall_smul_nonpos.

theorem Monovary.sub_smul_sub_nonneg {ι : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedRing α] [LinearOrderedAddCommGroup β] [Module α β] [OrderedSMul α β] {f : ι → α} {g : ι → β} : Monovary f g → ∀ (i j : ι), 0 ≤ (f j - f i) • (g j - g i)

Alias of the forward direction of monovary_iff_forall_smul_nonneg.

theorem Antivary.sub_smul_sub_nonpos {ι : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedRing α] [LinearOrderedAddCommGroup β] [Module α β] [OrderedSMul α β] {f : ι → α} {g : ι → β} : Antivary f g → ∀ (i j : ι), (f j - f i) • (g j - g i) ≤ 0

Alias of the forward direction of antivary_iff_forall_smul_nonpos.

theorem Monovary.smul_add_smul_le_smul_add_smul {ι : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedRing α] [LinearOrderedAddCommGroup β] [Module α β] [OrderedSMul α β] {f : ι → α} {g : ι → β} : Monovary f g → ∀ (i j : ι), f i • g j + f j • g i ≤ f i • g i + f j • g j

Alias of the forward direction of monovary_iff_smul_rearrangement.

---

Two functions monovary iff the rearrangement inequality holds.

theorem Antivary.smul_add_smul_le_smul_add_smul {ι : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedRing α] [LinearOrderedAddCommGroup β] [Module α β] [OrderedSMul α β] {f : ι → α} {g : ι → β} : Antivary f g → ∀ (i j : ι), f i • g i + f j • g j ≤ f i • g j + f j • g i

Alias of the forward direction of antivary_iff_smul_rearrangement.

---

Two functions antivary iff the rearrangement inequality holds.

theorem MonovaryOn.smul_add_smul_le_smul_add_smul {ι : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedRing α] [LinearOrderedAddCommGroup β] [Module α β] [OrderedSMul α β] {f : ι → α} {g : ι → β} {s : Set ι} : MonovaryOn f g s → ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → f i • g j + f j • g i ≤ f i • g i + f j • g j

Alias of the forward direction of monovaryOn_iff_smul_rearrangement.

---

Two functions monovary iff the rearrangement inequality holds.

theorem AntivaryOn.smul_add_smul_le_smul_add_smul {ι : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedRing α] [LinearOrderedAddCommGroup β] [Module α β] [OrderedSMul α β] {f : ι → α} {g : ι → β} {s : Set ι} : AntivaryOn f g s → ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → f i • g i + f j • g j ≤ f i • g j + f j • g i

Alias of the forward direction of antivaryOn_iff_smul_rearrangement.

---

Two functions antivary iff the rearrangement inequality holds.

theorem monovaryOn_iff_forall_mul_nonneg {ι : Type u_1} {α : Type u_2} [LinearOrderedRing α] {f : ι → α} {g : ι → α} {s : Set ι} : MonovaryOn f g s ↔ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → 0 ≤ (f j - f i) * (g j - g i)

theorem antivaryOn_iff_forall_mul_nonpos {ι : Type u_1} {α : Type u_2} [LinearOrderedRing α] {f : ι → α} {g : ι → α} {s : Set ι} : AntivaryOn f g s ↔ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → (f j - f i) * (g j - g i) ≤ 0

theorem monovary_iff_forall_mul_nonneg {ι : Type u_1} {α : Type u_2} [LinearOrderedRing α] {f : ι → α} {g : ι → α} : Monovary f g ↔ ∀ (i j : ι), 0 ≤ (f j - f i) * (g j - g i)

theorem antivary_iff_forall_mul_nonpos {ι : Type u_1} {α : Type u_2} [LinearOrderedRing α] {f : ι → α} {g : ι → α} : Antivary f g ↔ ∀ (i j : ι), (f j - f i) * (g j - g i) ≤ 0

theorem monovaryOn_iff_mul_rearrangement {ι : Type u_1} {α : Type u_2} [LinearOrderedRing α] {f : ι → α} {g : ι → α} {s : Set ι} : MonovaryOn f g s ↔ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → f i * g j + f j * g i ≤ f i * g i + f j * g j

Two functions monovary iff the rearrangement inequality holds.

theorem antivaryOn_iff_mul_rearrangement {ι : Type u_1} {α : Type u_2} [LinearOrderedRing α] {f : ι → α} {g : ι → α} {s : Set ι} : AntivaryOn f g s ↔ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → f i * g i + f j * g j ≤ f i * g j + f j * g i

Two functions antivary iff the rearrangement inequality holds.

theorem monovary_iff_mul_rearrangement {ι : Type u_1} {α : Type u_2} [LinearOrderedRing α] {f : ι → α} {g : ι → α} : Monovary f g ↔ ∀ (i j : ι), f i * g j + f j * g i ≤ f i * g i + f j * g j

Two functions monovary iff the rearrangement inequality holds.

theorem antivary_iff_mul_rearrangement {ι : Type u_1} {α : Type u_2} [LinearOrderedRing α] {f : ι → α} {g : ι → α} : Antivary f g ↔ ∀ (i j : ι), f i * g i + f j * g j ≤ f i * g j + f j * g i

Two functions antivary iff the rearrangement inequality holds.

theorem MonovaryOn.sub_mul_sub_nonneg {ι : Type u_1} {α : Type u_2} [LinearOrderedRing α] {f : ι → α} {g : ι → α} {s : Set ι} : MonovaryOn f g s → ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → 0 ≤ (f j - f i) * (g j - g i)

Alias of the forward direction of monovaryOn_iff_forall_mul_nonneg.

theorem AntivaryOn.sub_mul_sub_nonpos {ι : Type u_1} {α : Type u_2} [LinearOrderedRing α] {f : ι → α} {g : ι → α} {s : Set ι} : AntivaryOn f g s → ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → (f j - f i) * (g j - g i) ≤ 0

Alias of the forward direction of antivaryOn_iff_forall_mul_nonpos.

theorem Monovary.sub_mul_sub_nonneg {ι : Type u_1} {α : Type u_2} [LinearOrderedRing α] {f : ι → α} {g : ι → α} : Monovary f g → ∀ (i j : ι), 0 ≤ (f j - f i) * (g j - g i)

Alias of the forward direction of monovary_iff_forall_mul_nonneg.

theorem Antivary.sub_mul_sub_nonpos {ι : Type u_1} {α : Type u_2} [LinearOrderedRing α] {f : ι → α} {g : ι → α} : Antivary f g → ∀ (i j : ι), (f j - f i) * (g j - g i) ≤ 0

Alias of the forward direction of antivary_iff_forall_mul_nonpos.

theorem Monovary.mul_add_mul_le_mul_add_mul {ι : Type u_1} {α : Type u_2} [LinearOrderedRing α] {f : ι → α} {g : ι → α} : Monovary f g → ∀ (i j : ι), f i * g j + f j * g i ≤ f i * g i + f j * g j

Alias of the forward direction of monovary_iff_mul_rearrangement.

---

Two functions monovary iff the rearrangement inequality holds.

theorem Antivary.mul_add_mul_le_mul_add_mul {ι : Type u_1} {α : Type u_2} [LinearOrderedRing α] {f : ι → α} {g : ι → α} : Antivary f g → ∀ (i j : ι), f i * g i + f j * g j ≤ f i * g j + f j * g i

Alias of the forward direction of antivary_iff_mul_rearrangement.

---

Two functions antivary iff the rearrangement inequality holds.

theorem MonovaryOn.mul_add_mul_le_mul_add_mul {ι : Type u_1} {α : Type u_2} [LinearOrderedRing α] {f : ι → α} {g : ι → α} {s : Set ι} : MonovaryOn f g s → ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → f i * g j + f j * g i ≤ f i * g i + f j * g j

Alias of the forward direction of monovaryOn_iff_mul_rearrangement.

---

Two functions monovary iff the rearrangement inequality holds.

theorem AntivaryOn.mul_add_mul_le_mul_add_mul {ι : Type u_1} {α : Type u_2} [LinearOrderedRing α] {f : ι → α} {g : ι → α} {s : Set ι} : AntivaryOn f g s → ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → f i * g i + f j * g j ≤ f i * g j + f j * g i

Alias of the forward direction of antivaryOn_iff_mul_rearrangement.

---

Two functions antivary iff the rearrangement inequality holds.