mathlib documentation

algebra.module.ordered

Ordered module #

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 < 00 < c a

Alias 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 < 0c a < 0

Alias 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 < ac a < 0

Alias 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_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 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} (hc : c < 0) :
c a < b c⁻¹ b < a
theorem lt_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) :
a < c b b < c⁻¹ a
@[simp]
@[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
@[instance]
def prod.ordered_smul {k : Type u_1} {M : Type u_2} {N : Type u_3} [linear_ordered_field k] [ordered_add_comm_group M] [module k M] [ordered_smul k M] [ordered_add_comm_group N] [module k N] [ordered_smul k N] :
@[instance]
def pi.ordered_smul {k : Type u_1} [linear_ordered_field k] {ι : Type u_2} {M : ι → Type u_3} [Π (i : ι), ordered_add_comm_group (M i)] [Π (i : ι), mul_action_with_zero k (M i)] [∀ (i : ι), ordered_smul k (M i)] :
ordered_smul k (Π (i : ι), M i)
@[instance]
def pi.ordered_smul' {k : Type u_1} [linear_ordered_field k] {ι : Type u_2} {M : Type u_3} [ordered_add_comm_group M] [mul_action_with_zero k M] [ordered_smul k M] :
ordered_smul k (ι → M)

Upper/lower bounds #

theorem smul_lower_bounds_subset_lower_bounds_smul {k : Type u_1} {M : Type u_2} [ordered_semiring k] [ordered_add_comm_monoid M] [smul_with_zero k M] [ordered_smul k M] {s : set M} {c : k} (hc : 0 c) :
theorem smul_upper_bounds_subset_upper_bounds_smul {k : Type u_1} {M : Type u_2} [ordered_semiring k] [ordered_add_comm_monoid M] [smul_with_zero k M] [ordered_smul k M] {s : set M} {c : k} (hc : 0 c) :
theorem bdd_below.smul_of_nonneg {k : Type u_1} {M : Type u_2} [ordered_semiring k] [ordered_add_comm_monoid M] [smul_with_zero k M] [ordered_smul k M] {s : set M} {c : k} (hs : bdd_below s) (hc : 0 c) :
theorem bdd_above.smul_of_nonneg {k : Type u_1} {M : Type u_2} [ordered_semiring k] [ordered_add_comm_monoid M] [smul_with_zero k M] [ordered_smul k M] {s : set M} {c : k} (hs : bdd_above s) (hc : 0 c) :
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) :
@[simp]
theorem lower_bounds_smul_of_pos {k : Type u_1} {M : Type u_2} [linear_ordered_field k] [ordered_add_comm_group M] [mul_action_with_zero k M] [ordered_smul k M] {s : set M} {c : k} (hc : 0 < c) :
@[simp]
theorem upper_bounds_smul_of_pos {k : Type u_1} {M : Type u_2} [linear_ordered_field k] [ordered_add_comm_group M] [mul_action_with_zero k M] [ordered_smul k M] {s : set M} {c : k} (hc : 0 < c) :
@[simp]
theorem bdd_below_smul_iff_of_pos {k : Type u_1} {M : Type u_2} [linear_ordered_field k] [ordered_add_comm_group M] [mul_action_with_zero k M] [ordered_smul k M] {s : set M} {c : k} (hc : 0 < c) :
@[simp]
theorem bdd_above_smul_iff_of_pos {k : Type u_1} {M : Type u_2} [linear_ordered_field k] [ordered_add_comm_group M] [mul_action_with_zero k M] [ordered_smul k M] {s : set M} {c : k} (hc : 0 < c) :
@[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) :