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
@[protected, instance]
def
order_dual.module
{k : Type u_1}
{M : Type u_2}
[semiring k]
[ordered_add_comm_monoid M]
[module k M] :
module k (order_dual M)
Equations
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) :
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) :
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) :
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) :
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) :
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) :
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) :
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) :
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) :
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) :
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) :
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) :
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) :
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) :
@[simp]
theorem
order_iso.smul_left_dual_symm_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 : order_dual M) :
⇑(rel_iso.symm (order_iso.smul_left_dual M hc)) b = c⁻¹ • ⇑order_dual.of_dual b
@[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) :
⇑(order_iso.smul_left_dual M hc) b = ⇑order_dual.to_dual (c • b)
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) :
M ≃o order_dual M
Left scalar multiplication as an order isomorphism.
Equations
- order_iso.smul_left_dual M hc = {to_equiv := {to_fun := λ (b : M), ⇑order_dual.to_dual (c • b), inv_fun := λ (b : order_dual M), c⁻¹ • ⇑order_dual.of_dual b, left_inv := _, right_inv := _}, map_rel_iff' := _}
@[protected, 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] :
ordered_smul k (M × N)
@[protected, 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)
@[protected, 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) :
c • lower_bounds s ⊆ lower_bounds (c • s)
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) :
c • upper_bounds s ⊆ upper_bounds (c • s)
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) :
c • lower_bounds s ⊆ upper_bounds (c • s)
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) :
c • upper_bounds s ⊆ lower_bounds (c • s)
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) :
lower_bounds (c • s) = c • lower_bounds s
@[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) :
upper_bounds (c • s) = c • upper_bounds s
@[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) :
lower_bounds (c • s) = c • upper_bounds s
@[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) :
upper_bounds (c • s) = c • lower_bounds s
@[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) :