Ordered module #

In this file we provide lemmas about OrderedSMul that hold once a module structure is present.

References #

https://en.wikipedia.org/wiki/Ordered_vector_space

Tags #

ordered module, ordered scalar, ordered smul, ordered action, ordered vector space

theorem smul_neg_iff_of_pos {k : Type u_2} {M : Type u_3} [OrderedSemiring k] [OrderedAddCommGroup M] [Module k M] [OrderedSMul k M] {a : M} {c : k} (hc : 0 < c) :

c • a < 0 ↔ a < 0

source

theorem smul_lt_smul_of_neg {k : Type u_2} {M : Type u_3} [OrderedRing k] [OrderedAddCommGroup M] [Module k M] [OrderedSMul k M] {a : M} {b : M} {c : k} (h : a < b) (hc : c < 0) :

c • b < c • a

source

theorem smul_le_smul_of_nonpos {k : Type u_2} {M : Type u_3} [OrderedRing k] [OrderedAddCommGroup M] [Module k M] [OrderedSMul k M] {a : M} {b : M} {c : k} (h : a ≤ b) (hc : c ≤ 0) :

c • b ≤ c • a

source

theorem eq_of_smul_eq_smul_of_neg_of_le {k : Type u_2} {M : Type u_3} [OrderedRing k] [OrderedAddCommGroup M] [Module k M] [OrderedSMul k M] {a : M} {b : M} {c : k} (hab : c • a = c • b) (hc : c < 0) (h : a ≤ b) :

a = b

source

theorem lt_of_smul_lt_smul_of_nonpos {k : Type u_2} {M : Type u_3} [OrderedRing k] [OrderedAddCommGroup M] [Module k M] [OrderedSMul k M] {a : M} {b : M} {c : k} (h : c • a < c • b) (hc : c ≤ 0) :

b < a

source

theorem smul_le_smul_of_nonneg_right {k : Type u_2} {M : Type u_3} [OrderedRing k] [OrderedAddCommGroup M] [Module k M] [OrderedSMul k M] {b : M} {c : k} {d : k} (h : c ≤ d) (hb : 0 ≤ b) :

c • b ≤ d • b

source

theorem smul_le_smul {k : Type u_2} {M : Type u_3} [OrderedRing k] [OrderedAddCommGroup M] [Module k M] [OrderedSMul k M] {a : M} {b : M} {c : k} {d : k} (hcd : c ≤ d) (hab : a ≤ b) (hc : 0 ≤ c) (hb : 0 ≤ b) :

c • a ≤ d • b

source

theorem smul_lt_smul_iff_of_neg {k : Type u_2} {M : Type u_3} [OrderedRing k] [OrderedAddCommGroup M] [Module k M] [OrderedSMul k M] {a : M} {b : M} {c : k} (hc : c < 0) :

c • a < c • b ↔ b < a

source

theorem smul_neg_iff_of_neg {k : Type u_2} {M : Type u_3} [OrderedRing k] [OrderedAddCommGroup M] [Module k M] [OrderedSMul k M] {a : M} {c : k} (hc : c < 0) :

c • a < 0 ↔ 0 < a

source

theorem smul_pos_iff_of_neg {k : Type u_2} {M : Type u_3} [OrderedRing k] [OrderedAddCommGroup M] [Module k M] [OrderedSMul k M] {a : M} {c : k} (hc : c < 0) :

0 < c • a ↔ a < 0

source

theorem smul_nonpos_of_nonpos_of_nonneg {k : Type u_2} {M : Type u_3} [OrderedRing k] [OrderedAddCommGroup M] [Module k M] [OrderedSMul k M] {a : M} {c : k} (hc : c ≤ 0) (ha : 0 ≤ a) :

c • a ≤ 0

source

theorem smul_nonneg_of_nonpos_of_nonpos {k : Type u_2} {M : Type u_3} [OrderedRing k] [OrderedAddCommGroup M] [Module k M] [OrderedSMul k M] {a : M} {c : k} (hc : c ≤ 0) (ha : a ≤ 0) :

0 ≤ c • a

source

theorem smul_pos_of_neg_of_neg {k : Type u_2} {M : Type u_3} [OrderedRing k] [OrderedAddCommGroup M] [Module k M] [OrderedSMul k M] {a : M} {c : k} (hc : c < 0) :

a < 0 → 0 < c • a

Alias of the reverse direction of smul_pos_iff_of_neg.

source

theorem smul_neg_of_pos_of_neg {k : Type u_2} {M : Type u_3} [OrderedSemiring k] [OrderedAddCommGroup M] [Module k M] [OrderedSMul k M] {a : M} {c : k} (hc : 0 < c) :

a < 0 → c • a < 0

Alias of the reverse direction of smul_neg_iff_of_pos.

source

theorem smul_neg_of_neg_of_pos {k : Type u_2} {M : Type u_3} [OrderedRing k] [OrderedAddCommGroup M] [Module k M] [OrderedSMul k M] {a : M} {c : k} (hc : c < 0) :

0 < a → c • a < 0

Alias of the reverse direction of smul_neg_iff_of_neg.

source

theorem antitone_smul_left {k : Type u_2} {M : Type u_3} [OrderedRing k] [OrderedAddCommGroup M] [Module k M] [OrderedSMul k M] {c : k} (hc : c ≤ 0) :

Antitone (SMul.smul c)

source

theorem strict_anti_smul_left {k : Type u_2} {M : Type u_3} [OrderedRing k] [OrderedAddCommGroup M] [Module k M] [OrderedSMul k M] {c : k} (hc : c < 0) :

StrictAnti (SMul.smul c)

source

theorem smul_add_smul_le_smul_add_smul {k : Type u_2} {M : Type u_3} [OrderedRing k] [OrderedAddCommGroup M] [Module k M] [OrderedSMul k M] [ContravariantClass M M (fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x ≤ x_1] {a : k} {b : k} {c : M} {d : M} (hab : a ≤ b) (hcd : c ≤ d) :

a • d + b • c ≤ a • c + b • d

Binary rearrangement inequality.

source

theorem smul_add_smul_le_smul_add_smul' {k : Type u_2} {M : Type u_3} [OrderedRing k] [OrderedAddCommGroup M] [Module k M] [OrderedSMul k M] [ContravariantClass M M (fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x ≤ x_1] {a : k} {b : k} {c : M} {d : M} (hba : b ≤ a) (hdc : d ≤ c) :

a • d + b • c ≤ a • c + b • d

Binary rearrangement inequality.

source

theorem smul_add_smul_lt_smul_add_smul {k : Type u_2} {M : Type u_3} [OrderedRing k] [OrderedAddCommGroup M] [Module k M] [OrderedSMul k M] [CovariantClass M M (fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x < x_1] [ContravariantClass M M (fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x < x_1] {a : k} {b : k} {c : M} {d : M} (hab : a < b) (hcd : c < d) :

a • d + b • c < a • c + b • d

Binary strict rearrangement inequality.

source

theorem smul_add_smul_lt_smul_add_smul' {k : Type u_2} {M : Type u_3} [OrderedRing k] [OrderedAddCommGroup M] [Module k M] [OrderedSMul k M] [CovariantClass M M (fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x < x_1] [ContravariantClass M M (fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x < x_1] {a : k} {b : k} {c : M} {d : M} (hba : b < a) (hdc : d < c) :

a • d + b • c < a • c + b • d

Binary strict rearrangement inequality.

source

theorem smul_le_smul_iff_of_neg {k : Type u_2} {M : Type u_3} [LinearOrderedField k] [OrderedAddCommGroup M] [Module k M] [OrderedSMul k M] {a : M} {b : M} {c : k} (hc : c < 0) :

c • a ≤ c • b ↔ b ≤ a

source

theorem inv_smul_le_iff_of_neg {k : Type u_2} {M : Type u_3} [LinearOrderedField k] [OrderedAddCommGroup M] [Module k M] [OrderedSMul k M] {a : M} {b : M} {c : k} (h : c < 0) :

c⁻¹ • a ≤ b ↔ c • b ≤ a

source

theorem inv_smul_lt_iff_of_neg {k : Type u_2} {M : Type u_3} [LinearOrderedField k] [OrderedAddCommGroup M] [Module k M] [OrderedSMul k M] {a : M} {b : M} {c : k} (h : c < 0) :

c⁻¹ • a < b ↔ c • b < a

source

theorem smul_inv_le_iff_of_neg {k : Type u_2} {M : Type u_3} [LinearOrderedField k] [OrderedAddCommGroup M] [Module k M] [OrderedSMul k M] {a : M} {b : M} {c : k} (h : c < 0) :

a ≤ c⁻¹ • b ↔ b ≤ c • a

source

theorem smul_inv_lt_iff_of_neg {k : Type u_2} {M : Type u_3} [LinearOrderedField k] [OrderedAddCommGroup M] [Module k M] [OrderedSMul k M] {a : M} {b : M} {c : k} (h : c < 0) :

a < c⁻¹ • b ↔ b < c • a

source

@[simp]

theorem OrderIso.smulLeftDual_apply {k : Type u_2} (M : Type u_3) [LinearOrderedField k] [OrderedAddCommGroup M] [Module k M] [OrderedSMul k M] {c : k} (hc : c < 0) (b : M) :

(OrderIso.smulLeftDual M hc) b = OrderDual.toDual (c • b)

source

@[simp]

theorem OrderIso.smulLeftDual_symm_apply {k : Type u_2} (M : Type u_3) [LinearOrderedField k] [OrderedAddCommGroup M] [Module k M] [OrderedSMul k M] {c : k} (hc : c < 0) (b : Mᵒᵈ) :

(RelIso.symm (OrderIso.smulLeftDual M hc)) b = c⁻¹ • OrderDual.ofDual b

source

def OrderIso.smulLeftDual {k : Type u_2} (M : Type u_3) [LinearOrderedField k] [OrderedAddCommGroup M] [Module k M] [OrderedSMul k M] {c : k} (hc : c < 0) :

M ≃o Mᵒᵈ

Left scalar multiplication as an order isomorphism.

Equations

One or more equations did not get rendered due to their size.

Instances For

Upper/lower bounds #

source

theorem smul_lowerBounds_subset_upperBounds_smul {k : Type u_2} {M : Type u_3} [OrderedRing k] [OrderedAddCommGroup M] [Module k M] [OrderedSMul k M] {s : Set M} {c : k} (hc : c ≤ 0) :

c • lowerBounds s ⊆ upperBounds (c • s)

source

theorem smul_upperBounds_subset_lowerBounds_smul {k : Type u_2} {M : Type u_3} [OrderedRing k] [OrderedAddCommGroup M] [Module k M] [OrderedSMul k M] {s : Set M} {c : k} (hc : c ≤ 0) :

c • upperBounds s ⊆ lowerBounds (c • s)

source

theorem BddBelow.smul_of_nonpos {k : Type u_2} {M : Type u_3} [OrderedRing k] [OrderedAddCommGroup M] [Module k M] [OrderedSMul k M] {s : Set M} {c : k} (hc : c ≤ 0) (hs : BddBelow s) :

BddAbove (c • s)

source

theorem BddAbove.smul_of_nonpos {k : Type u_2} {M : Type u_3} [OrderedRing k] [OrderedAddCommGroup M] [Module k M] [OrderedSMul k M] {s : Set M} {c : k} (hc : c ≤ 0) (hs : BddAbove s) :

BddBelow (c • s)

source

theorem smul_max_of_nonpos {k : Type u_2} {M : Type u_3} [LinearOrderedRing k] [LinearOrderedAddCommGroup M] [Module k M] [OrderedSMul k M] {a : k} (ha : a ≤ 0) (b₁ : M) (b₂ : M) :

a • max b₁ b₂ = min (a • b₁) (a • b₂)

source

theorem smul_min_of_nonpos {k : Type u_2} {M : Type u_3} [LinearOrderedRing k] [LinearOrderedAddCommGroup M] [Module k M] [OrderedSMul k M] {a : k} (ha : a ≤ 0) (b₁ : M) (b₂ : M) :

a • min b₁ b₂ = max (a • b₁) (a • b₂)

source

theorem nonneg_and_nonneg_or_nonpos_and_nonpos_of_smul_nonneg {k : Type u_2} {M : Type u_3} [LinearOrderedRing k] [LinearOrderedAddCommGroup M] [Module k M] [OrderedSMul k M] {a : k} {b : M} (hab : 0 ≤ a • b) :

0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0

source

theorem smul_nonneg_iff {k : Type u_2} {M : Type u_3} [LinearOrderedRing k] [LinearOrderedAddCommGroup M] [Module k M] [OrderedSMul k M] {a : k} {b : M} :

0 ≤ a • b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0

source

theorem smul_nonpos_iff {k : Type u_2} {M : Type u_3} [LinearOrderedRing k] [LinearOrderedAddCommGroup M] [Module k M] [OrderedSMul k M] {a : k} {b : M} :

a • b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b

source

theorem smul_nonneg_iff_pos_imp_nonneg {k : Type u_2} {M : Type u_3} [LinearOrderedRing k] [LinearOrderedAddCommGroup M] [Module k M] [OrderedSMul k M] {a : k} {b : M} :

0 ≤ a • b ↔ (0 < a → 0 ≤ b) ∧ (0 < b → 0 ≤ a)

source

theorem smul_nonneg_iff_neg_imp_nonpos {k : Type u_2} {M : Type u_3} [LinearOrderedRing k] [LinearOrderedAddCommGroup M] [Module k M] [OrderedSMul k M] {a : k} {b : M} :

0 ≤ a • b ↔ (a < 0 → b ≤ 0) ∧ (b < 0 → a ≤ 0)

source

theorem smul_nonpos_iff_pos_imp_nonpos {k : Type u_2} {M : Type u_3} [LinearOrderedRing k] [LinearOrderedAddCommGroup M] [Module k M] [OrderedSMul k M] {a : k} {b : M} :

a • b ≤ 0 ↔ (0 < a → b ≤ 0) ∧ (b < 0 → 0 ≤ a)

source

theorem smul_nonpos_iff_neg_imp_nonneg {k : Type u_2} {M : Type u_3} [LinearOrderedRing k] [LinearOrderedAddCommGroup M] [Module k M] [OrderedSMul k M] {a : k} {b : M} :

a • b ≤ 0 ↔ (a < 0 → 0 ≤ b) ∧ (0 < b → a ≤ 0)

source

@[simp]

theorem lowerBounds_smul_of_neg {k : Type u_2} {M : Type u_3} [LinearOrderedField k] [OrderedAddCommGroup M] [Module k M] [OrderedSMul k M] {s : Set M} {c : k} (hc : c < 0) :

lowerBounds (c • s) = c • upperBounds s

source

@[simp]

theorem upperBounds_smul_of_neg {k : Type u_2} {M : Type u_3} [LinearOrderedField k] [OrderedAddCommGroup M] [Module k M] [OrderedSMul k M] {s : Set M} {c : k} (hc : c < 0) :

upperBounds (c • s) = c • lowerBounds s

source

@[simp]

theorem bddBelow_smul_iff_of_neg {k : Type u_2} {M : Type u_3} [LinearOrderedField k] [OrderedAddCommGroup M] [Module k M] [OrderedSMul k M] {s : Set M} {c : k} (hc : c < 0) :

BddBelow (c • s) ↔ BddAbove s

source

@[simp]

theorem bddAbove_smul_iff_of_neg {k : Type u_2} {M : Type u_3} [LinearOrderedField k] [OrderedAddCommGroup M] [Module k M] [OrderedSMul k M] {s : Set M} {c : k} (hc : c < 0) :

BddAbove (c • s) ↔ BddBelow s