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_module

Tags #

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

source

instance instModuleOrderDual {k : Type u_1} {M : Type u_2} [Semiring k] [OrderedAddCommMonoid M] [Module k M] :

Module k Mᵒᵈ

Equations

instModuleOrderDual = Module.mk (_ : ∀ (x x_1 : k) (x_2 : Mᵒᵈ), (x + x_1) • x_2 = x • x_2 + x_1 • x_2) (_ : ∀ (m : Mᵒᵈ), 0 • m = 0)

source

theorem smul_neg_iff_of_pos {k : Type u_1} {M : Type u_2} [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_1} {M : Type u_2} [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_1} {M : Type u_2} [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_1} {M : Type u_2} [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_1} {M : Type u_2} [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_lt_smul_iff_of_neg {k : Type u_1} {M : Type u_2} [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_1} {M : Type u_2} [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_1} {M : Type u_2} [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_1} {M : Type u_2} [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_1} {M : Type u_2} [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_1} {M : Type u_2} [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_1} {M : Type u_2} [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_1} {M : Type u_2} [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_1} {M : Type u_2} [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_1} {M : Type u_2} [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_1} {M : Type u_2} [OrderedRing k] [OrderedAddCommGroup M] [Module k M] [OrderedSMul k M] [ContravariantClass M M (fun x x_1 => x + x_1) fun x x_1 => 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_1} {M : Type u_2} [OrderedRing k] [OrderedAddCommGroup M] [Module k M] [OrderedSMul k M] [ContravariantClass M M (fun x x_1 => x + x_1) fun x x_1 => 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_1} {M : Type u_2} [OrderedRing k] [OrderedAddCommGroup M] [Module k M] [OrderedSMul k M] [CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1] [ContravariantClass M M (fun x x_1 => x + x_1) fun x x_1 => 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_1} {M : Type u_2} [OrderedRing k] [OrderedAddCommGroup M] [Module k M] [OrderedSMul k M] [CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1] [ContravariantClass M M (fun x x_1 => x + x_1) fun x x_1 => 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_1} {M : Type u_2} [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_1} {M : Type u_2} [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_1} {M : Type u_2} [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_1} {M : Type u_2} [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_1} {M : Type u_2} [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_symm_apply {k : Type u_1} (M : Type u_2) [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

@[simp]

theorem OrderIso.smulLeftDual_apply {k : Type u_1} (M : Type u_2) [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

def OrderIso.smulLeftDual {k : Type u_1} (M : Type u_2) [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_1} {M : Type u_2} [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_1} {M : Type u_2} [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_1} {M : Type u_2} [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_1} {M : Type u_2} [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

@[simp]

theorem lowerBounds_smul_of_neg {k : Type u_1} {M : Type u_2} [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_1} {M : Type u_2} [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_1} {M : Type u_2} [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_1} {M : Type u_2} [LinearOrderedField k] [OrderedAddCommGroup M] [Module k M] [OrderedSMul k M] {s : Set M} {c : k} (hc : c < 0) :

BddAbove (c • s) ↔ BddBelow s