mathlib3 documentation

algebra.order.upper_lower

Algebraic operations on upper/lower sets #

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

Upper/lower sets are preserved under pointwise algebraic operations in ordered groups.

theorem is_upper_set.vadd_subset {α : Type u_1} [ordered_add_comm_monoid α] {s : set α} {x : α} (hs : is_upper_set s) (hx : 0 x) :
x +ᵥ s s
theorem is_upper_set.smul_subset {α : Type u_1} [ordered_comm_monoid α] {s : set α} {x : α} (hs : is_upper_set s) (hx : 1 x) :
x s s
theorem is_lower_set.vadd_subset {α : Type u_1} [ordered_add_comm_monoid α] {s : set α} {x : α} (hs : is_lower_set s) (hx : x 0) :
x +ᵥ s s
theorem is_lower_set.smul_subset {α : Type u_1} [ordered_comm_monoid α] {s : set α} {x : α} (hs : is_lower_set s) (hx : x 1) :
x s s
theorem is_upper_set.vadd {α : Type u_1} [ordered_add_comm_group α] {s : set α} {a : α} (hs : is_upper_set s) :
theorem is_upper_set.smul {α : Type u_1} [ordered_comm_group α] {s : set α} {a : α} (hs : is_upper_set s) :
theorem is_lower_set.smul {α : Type u_1} [ordered_comm_group α] {s : set α} {a : α} (hs : is_lower_set s) :
theorem is_lower_set.vadd {α : Type u_1} [ordered_add_comm_group α] {s : set α} {a : α} (hs : is_lower_set s) :
theorem set.ord_connected.vadd {α : Type u_1} [ordered_add_comm_group α] {s : set α} {a : α} (hs : s.ord_connected) :
theorem set.ord_connected.smul {α : Type u_1} [ordered_comm_group α] {s : set α} {a : α} (hs : s.ord_connected) :
theorem is_upper_set.add_left {α : Type u_1} [ordered_add_comm_group α] {s t : set α} (ht : is_upper_set t) :
theorem is_upper_set.mul_left {α : Type u_1} [ordered_comm_group α] {s t : set α} (ht : is_upper_set t) :
theorem is_upper_set.mul_right {α : Type u_1} [ordered_comm_group α] {s t : set α} (hs : is_upper_set s) :
theorem is_upper_set.add_right {α : Type u_1} [ordered_add_comm_group α] {s t : set α} (hs : is_upper_set s) :
theorem is_lower_set.mul_left {α : Type u_1} [ordered_comm_group α] {s t : set α} (ht : is_lower_set t) :
theorem is_lower_set.add_left {α : Type u_1} [ordered_add_comm_group α] {s t : set α} (ht : is_lower_set t) :
theorem is_lower_set.mul_right {α : Type u_1} [ordered_comm_group α] {s t : set α} (hs : is_lower_set s) :
theorem is_lower_set.add_right {α : Type u_1} [ordered_add_comm_group α] {s t : set α} (hs : is_lower_set s) :
theorem is_upper_set.neg {α : Type u_1} [ordered_add_comm_group α] {s : set α} (hs : is_upper_set s) :
theorem is_upper_set.inv {α : Type u_1} [ordered_comm_group α] {s : set α} (hs : is_upper_set s) :
theorem is_lower_set.inv {α : Type u_1} [ordered_comm_group α] {s : set α} (hs : is_lower_set s) :
theorem is_lower_set.neg {α : Type u_1} [ordered_add_comm_group α] {s : set α} (hs : is_lower_set s) :
theorem is_upper_set.div_left {α : Type u_1} [ordered_comm_group α] {s t : set α} (ht : is_upper_set t) :
theorem is_upper_set.sub_left {α : Type u_1} [ordered_add_comm_group α] {s t : set α} (ht : is_upper_set t) :
theorem is_upper_set.sub_right {α : Type u_1} [ordered_add_comm_group α] {s t : set α} (hs : is_upper_set s) :
theorem is_upper_set.div_right {α : Type u_1} [ordered_comm_group α] {s t : set α} (hs : is_upper_set s) :
theorem is_lower_set.div_left {α : Type u_1} [ordered_comm_group α] {s t : set α} (ht : is_lower_set t) :
theorem is_lower_set.sub_left {α : Type u_1} [ordered_add_comm_group α] {s t : set α} (ht : is_lower_set t) :
theorem is_lower_set.sub_right {α : Type u_1} [ordered_add_comm_group α] {s t : set α} (hs : is_lower_set s) :
theorem is_lower_set.div_right {α : Type u_1} [ordered_comm_group α] {s t : set α} (hs : is_lower_set s) :
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp, norm_cast]
theorem upper_set.coe_one {α : Type u_1} [ordered_comm_group α] :
@[simp, norm_cast]
theorem upper_set.coe_zero {α : Type u_1} [ordered_add_comm_group α] :
@[simp, norm_cast]
theorem upper_set.coe_smul {α : Type u_1} [ordered_comm_group α] (a : α) (s : upper_set α) :
(a s) = a s
@[simp, norm_cast]
theorem upper_set.coe_vadd {α : Type u_1} [ordered_add_comm_group α] (a : α) (s : upper_set α) :
(a +ᵥ s) = a +ᵥ s
@[simp, norm_cast]
theorem upper_set.coe_mul {α : Type u_1} [ordered_comm_group α] (s t : upper_set α) :
(s * t) = s * t
@[simp, norm_cast]
theorem upper_set.coe_add {α : Type u_1} [ordered_add_comm_group α] (s t : upper_set α) :
(s + t) = s + t
@[simp, norm_cast]
theorem upper_set.coe_div {α : Type u_1} [ordered_comm_group α] (s t : upper_set α) :
(s / t) = s / t
@[simp, norm_cast]
theorem upper_set.coe_sub {α : Type u_1} [ordered_add_comm_group α] (s t : upper_set α) :
(s - t) = s - t
@[simp]
theorem upper_set.Ici_one {α : Type u_1} [ordered_comm_group α] :
@[simp]
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp, norm_cast]
theorem lower_set.coe_smul {α : Type u_1} [ordered_comm_group α] (a : α) (s : lower_set α) :
(a s) = a s
@[simp, norm_cast]
theorem lower_set.coe_vadd {α : Type u_1} [ordered_add_comm_group α] (a : α) (s : lower_set α) :
(a +ᵥ s) = a +ᵥ s
@[simp, norm_cast]
theorem lower_set.coe_mul {α : Type u_1} [ordered_comm_group α] (s t : lower_set α) :
(s * t) = s * t
@[simp, norm_cast]
theorem lower_set.coe_add {α : Type u_1} [ordered_add_comm_group α] (s t : lower_set α) :
(s + t) = s + t
@[simp, norm_cast]
theorem lower_set.coe_sub {α : Type u_1} [ordered_add_comm_group α] (s t : lower_set α) :
(s - t) = s - t
@[simp, norm_cast]
theorem lower_set.coe_div {α : Type u_1} [ordered_comm_group α] (s t : lower_set α) :
(s / t) = s / t
@[simp]
theorem lower_set.Iic_one {α : Type u_1} [ordered_comm_group α] :
@[simp]
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp]
theorem upper_closure_one {α : Type u_1} [ordered_comm_group α] :
@[simp]
@[simp]
@[simp]
theorem lower_closure_one {α : Type u_1} [ordered_comm_group α] :
@[simp]
theorem upper_closure_vadd {α : Type u_1} [ordered_add_comm_group α] (s : set α) (a : α) :
@[simp]
theorem upper_closure_smul {α : Type u_1} [ordered_comm_group α] (s : set α) (a : α) :
@[simp]
theorem lower_closure_smul {α : Type u_1} [ordered_comm_group α] (s : set α) (a : α) :
@[simp]
theorem lower_closure_vadd {α : Type u_1} [ordered_add_comm_group α] (s : set α) (a : α) :
theorem mul_upper_closure {α : Type u_1} [ordered_comm_group α] (s t : set α) :
theorem add_upper_closure {α : Type u_1} [ordered_add_comm_group α] (s t : set α) :
theorem mul_lower_closure {α : Type u_1} [ordered_comm_group α] (s t : set α) :
theorem add_lower_closure {α : Type u_1} [ordered_add_comm_group α] (s t : set α) :
theorem upper_closure_add {α : Type u_1} [ordered_add_comm_group α] (s t : set α) :
theorem upper_closure_mul {α : Type u_1} [ordered_comm_group α] (s t : set α) :
theorem lower_closure_add {α : Type u_1} [ordered_add_comm_group α] (s t : set α) :
theorem lower_closure_mul {α : Type u_1} [ordered_comm_group α] (s t : set α) :
@[simp]
@[simp]
@[simp]
@[simp]