mathlib3 documentation

algebra.order.module

Ordered module #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

References #

Tags #

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

theorem smul_neg_iff_of_pos {k : Type u_1} {M : Type u_2} [ordered_semiring k] [ordered_add_comm_group M] [module k M] [ordered_smul k M] {a : M} {c : k} (hc : 0 < c) :
c a < 0 a < 0
theorem smul_lt_smul_of_neg {k : Type u_1} {M : Type u_2} [ordered_ring k] [ordered_add_comm_group M] [module k M] [ordered_smul k M] {a b : M} {c : k} (h : a < b) (hc : c < 0) :
c b < c a
theorem smul_le_smul_of_nonpos {k : Type u_1} {M : Type u_2} [ordered_ring k] [ordered_add_comm_group M] [module k M] [ordered_smul k M] {a b : M} {c : k} (h : a b) (hc : c 0) :
c b c a
theorem eq_of_smul_eq_smul_of_neg_of_le {k : Type u_1} {M : Type u_2} [ordered_ring k] [ordered_add_comm_group M] [module k M] [ordered_smul k M] {a b : M} {c : k} (hab : c a = c b) (hc : c < 0) (h : a b) :
a = b
theorem lt_of_smul_lt_smul_of_nonpos {k : Type u_1} {M : Type u_2} [ordered_ring k] [ordered_add_comm_group M] [module k M] [ordered_smul k M] {a b : M} {c : k} (h : c a < c b) (hc : c 0) :
b < a
theorem smul_lt_smul_iff_of_neg {k : Type u_1} {M : Type u_2} [ordered_ring k] [ordered_add_comm_group M] [module k M] [ordered_smul k M] {a b : M} {c : k} (hc : c < 0) :
c a < c b b < a
theorem smul_neg_iff_of_neg {k : Type u_1} {M : Type u_2} [ordered_ring k] [ordered_add_comm_group M] [module k M] [ordered_smul k M] {a : M} {c : k} (hc : c < 0) :
c a < 0 0 < a
theorem smul_pos_iff_of_neg {k : Type u_1} {M : Type u_2} [ordered_ring k] [ordered_add_comm_group M] [module k M] [ordered_smul k M] {a : M} {c : k} (hc : c < 0) :
0 < c a a < 0
theorem smul_nonpos_of_nonpos_of_nonneg {k : Type u_1} {M : Type u_2} [ordered_ring k] [ordered_add_comm_group M] [module k M] [ordered_smul k M] {a : M} {c : k} (hc : c 0) (ha : 0 a) :
c a 0
theorem smul_nonneg_of_nonpos_of_nonpos {k : Type u_1} {M : Type u_2} [ordered_ring k] [ordered_add_comm_group M] [module k M] [ordered_smul k M] {a : M} {c : k} (hc : c 0) (ha : a 0) :
0 c a
theorem smul_pos_of_neg_of_neg {k : Type u_1} {M : Type u_2} [ordered_ring k] [ordered_add_comm_group M] [module k M] [ordered_smul 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.

theorem smul_neg_of_pos_of_neg {k : Type u_1} {M : Type u_2} [ordered_semiring k] [ordered_add_comm_group M] [module k M] [ordered_smul 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.

theorem smul_neg_of_neg_of_pos {k : Type u_1} {M : Type u_2} [ordered_ring k] [ordered_add_comm_group M] [module k M] [ordered_smul 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.

theorem antitone_smul_left {k : Type u_1} {M : Type u_2} [ordered_ring k] [ordered_add_comm_group M] [module k M] [ordered_smul k M] {c : k} (hc : c 0) :
theorem strict_anti_smul_left {k : Type u_1} {M : Type u_2} [ordered_ring k] [ordered_add_comm_group M] [module k M] [ordered_smul k M] {c : k} (hc : c < 0) :
theorem smul_add_smul_le_smul_add_smul {k : Type u_1} {M : Type u_2} [ordered_ring k] [ordered_add_comm_group M] [module k M] [ordered_smul k M] [contravariant_class M M has_add.add has_le.le] {a b : k} {c d : M} (hab : a b) (hcd : c d) :
a d + b c a c + b d

Binary rearrangement inequality.

theorem smul_add_smul_le_smul_add_smul' {k : Type u_1} {M : Type u_2} [ordered_ring k] [ordered_add_comm_group M] [module k M] [ordered_smul k M] [contravariant_class M M has_add.add has_le.le] {a b : k} {c d : M} (hba : b a) (hdc : d c) :
a d + b c a c + b d

Binary rearrangement inequality.

theorem smul_add_smul_lt_smul_add_smul {k : Type u_1} {M : Type u_2} [ordered_ring k] [ordered_add_comm_group M] [module k M] [ordered_smul k M] [covariant_class M M has_add.add has_lt.lt] [contravariant_class M M has_add.add has_lt.lt] {a b : k} {c d : M} (hab : a < b) (hcd : c < d) :
a d + b c < a c + b d

Binary strict rearrangement inequality.

theorem smul_add_smul_lt_smul_add_smul' {k : Type u_1} {M : Type u_2} [ordered_ring k] [ordered_add_comm_group M] [module k M] [ordered_smul k M] [covariant_class M M has_add.add has_lt.lt] [contravariant_class M M has_add.add has_lt.lt] {a b : k} {c d : M} (hba : b < a) (hdc : d < c) :
a d + b c < a c + b d

Binary strict rearrangement inequality.

theorem smul_le_smul_iff_of_neg {k : Type u_1} {M : Type u_2} [linear_ordered_field k] [ordered_add_comm_group M] [module k M] [ordered_smul k M] {a b : M} {c : k} (hc : c < 0) :
c a c b b a
theorem inv_smul_le_iff_of_neg {k : Type u_1} {M : Type u_2} [linear_ordered_field k] [ordered_add_comm_group M] [module k M] [ordered_smul k M] {a b : M} {c : k} (h : c < 0) :
c⁻¹ a b c b a
theorem inv_smul_lt_iff_of_neg {k : Type u_1} {M : Type u_2} [linear_ordered_field k] [ordered_add_comm_group M] [module k M] [ordered_smul k M] {a b : M} {c : k} (h : c < 0) :
c⁻¹ a < b c b < a
theorem smul_inv_le_iff_of_neg {k : Type u_1} {M : Type u_2} [linear_ordered_field k] [ordered_add_comm_group M] [module k M] [ordered_smul k M] {a b : M} {c : k} (h : c < 0) :
a c⁻¹ b b c a
theorem smul_inv_lt_iff_of_neg {k : Type u_1} {M : Type u_2} [linear_ordered_field k] [ordered_add_comm_group M] [module k M] [ordered_smul k M] {a b : M} {c : k} (h : c < 0) :
a < c⁻¹ b b < c a
@[simp]
theorem order_iso.smul_left_dual_apply {k : Type u_1} (M : Type u_2) [linear_ordered_field k] [ordered_add_comm_group M] [module k M] [ordered_smul k M] {c : k} (hc : c < 0) (b : M) :
def order_iso.smul_left_dual {k : Type u_1} (M : Type u_2) [linear_ordered_field k] [ordered_add_comm_group M] [module k M] [ordered_smul k M] {c : k} (hc : c < 0) :

Left scalar multiplication as an order isomorphism.

Equations

Upper/lower bounds #

theorem smul_lower_bounds_subset_upper_bounds_smul {k : Type u_1} {M : Type u_2} [ordered_ring k] [ordered_add_comm_group M] [module k M] [ordered_smul k M] {s : set M} {c : k} (hc : c 0) :
theorem smul_upper_bounds_subset_lower_bounds_smul {k : Type u_1} {M : Type u_2} [ordered_ring k] [ordered_add_comm_group M] [module k M] [ordered_smul k M] {s : set M} {c : k} (hc : c 0) :
theorem bdd_below.smul_of_nonpos {k : Type u_1} {M : Type u_2} [ordered_ring k] [ordered_add_comm_group M] [module k M] [ordered_smul k M] {s : set M} {c : k} (hc : c 0) (hs : bdd_below s) :
theorem bdd_above.smul_of_nonpos {k : Type u_1} {M : Type u_2} [ordered_ring k] [ordered_add_comm_group M] [module k M] [ordered_smul k M] {s : set M} {c : k} (hc : c 0) (hs : bdd_above s) :
theorem smul_max_of_nonpos {k : Type u_1} {M : Type u_2} [linear_ordered_ring k] [linear_ordered_add_comm_group M] [module k M] [ordered_smul k M] {a : k} (ha : a 0) (b₁ b₂ : M) :
a linear_order.max b₁ b₂ = linear_order.min (a b₁) (a b₂)
theorem smul_min_of_nonpos {k : Type u_1} {M : Type u_2} [linear_ordered_ring k] [linear_ordered_add_comm_group M] [module k M] [ordered_smul k M] {a : k} (ha : a 0) (b₁ b₂ : M) :
a linear_order.min b₁ b₂ = linear_order.max (a b₁) (a b₂)
@[simp]
theorem lower_bounds_smul_of_neg {k : Type u_1} {M : Type u_2} [linear_ordered_field k] [ordered_add_comm_group M] [module k M] [ordered_smul k M] {s : set M} {c : k} (hc : c < 0) :
@[simp]
theorem upper_bounds_smul_of_neg {k : Type u_1} {M : Type u_2} [linear_ordered_field k] [ordered_add_comm_group M] [module k M] [ordered_smul k M] {s : set M} {c : k} (hc : c < 0) :
@[simp]
theorem bdd_below_smul_iff_of_neg {k : Type u_1} {M : Type u_2} [linear_ordered_field k] [ordered_add_comm_group M] [module k M] [ordered_smul k M] {s : set M} {c : k} (hc : c < 0) :
@[simp]
theorem bdd_above_smul_iff_of_neg {k : Type u_1} {M : Type u_2} [linear_ordered_field k] [ordered_add_comm_group M] [module k M] [ordered_smul k M] {s : set M} {c : k} (hc : c < 0) :