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
@[protected, instance]
def
order_dual.module
{k : Type u_1}
{M : Type u_2}
[semiring k]
[ordered_add_comm_monoid M]
[module k 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 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) :
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) :
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) :
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) :
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) :
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) :
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) :
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) :
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) :
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) :
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) :
@[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 : 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) :
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 : Mᵒᵈ), c⁻¹ • ⇑order_dual.of_dual b, left_inv := _, right_inv := _}, map_rel_iff' := _}
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) :
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) :
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) :
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) :