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) :
theorem
is_upper_set.smul_subset
{α : Type u_1}
[ordered_comm_monoid α]
{s : set α}
{x : α}
(hs : is_upper_set s)
(hx : 1 ≤ x) :
theorem
is_lower_set.vadd_subset
{α : Type u_1}
[ordered_add_comm_monoid α]
{s : set α}
{x : α}
(hs : is_lower_set s)
(hx : x ≤ 0) :
theorem
is_lower_set.smul_subset
{α : Type u_1}
[ordered_comm_monoid α]
{s : set α}
{x : α}
(hs : is_lower_set s)
(hx : x ≤ 1) :
theorem
is_upper_set.vadd
{α : Type u_1}
[ordered_add_comm_group α]
{s : set α}
{a : α}
(hs : is_upper_set s) :
is_upper_set (a +ᵥ s)
theorem
is_upper_set.smul
{α : Type u_1}
[ordered_comm_group α]
{s : set α}
{a : α}
(hs : is_upper_set s) :
is_upper_set (a • s)
theorem
is_lower_set.smul
{α : Type u_1}
[ordered_comm_group α]
{s : set α}
{a : α}
(hs : is_lower_set s) :
is_lower_set (a • s)
theorem
is_lower_set.vadd
{α : Type u_1}
[ordered_add_comm_group α]
{s : set α}
{a : α}
(hs : is_lower_set s) :
is_lower_set (a +ᵥ s)
theorem
set.ord_connected.vadd
{α : Type u_1}
[ordered_add_comm_group α]
{s : set α}
{a : α}
(hs : s.ord_connected) :
(a +ᵥ s).ord_connected
theorem
set.ord_connected.smul
{α : Type u_1}
[ordered_comm_group α]
{s : set α}
{a : α}
(hs : s.ord_connected) :
(a • s).ord_connected
theorem
is_upper_set.add_left
{α : Type u_1}
[ordered_add_comm_group α]
{s t : set α}
(ht : is_upper_set t) :
is_upper_set (s + t)
theorem
is_upper_set.mul_left
{α : Type u_1}
[ordered_comm_group α]
{s t : set α}
(ht : is_upper_set t) :
is_upper_set (s * t)
theorem
is_upper_set.mul_right
{α : Type u_1}
[ordered_comm_group α]
{s t : set α}
(hs : is_upper_set s) :
is_upper_set (s * t)
theorem
is_upper_set.add_right
{α : Type u_1}
[ordered_add_comm_group α]
{s t : set α}
(hs : is_upper_set s) :
is_upper_set (s + t)
theorem
is_lower_set.mul_left
{α : Type u_1}
[ordered_comm_group α]
{s t : set α}
(ht : is_lower_set t) :
is_lower_set (s * t)
theorem
is_lower_set.add_left
{α : Type u_1}
[ordered_add_comm_group α]
{s t : set α}
(ht : is_lower_set t) :
is_lower_set (s + t)
theorem
is_lower_set.mul_right
{α : Type u_1}
[ordered_comm_group α]
{s t : set α}
(hs : is_lower_set s) :
is_lower_set (s * t)
theorem
is_lower_set.add_right
{α : Type u_1}
[ordered_add_comm_group α]
{s t : set α}
(hs : is_lower_set s) :
is_lower_set (s + t)
theorem
is_upper_set.neg
{α : Type u_1}
[ordered_add_comm_group α]
{s : set α}
(hs : is_upper_set s) :
is_lower_set (-s)
theorem
is_lower_set.neg
{α : Type u_1}
[ordered_add_comm_group α]
{s : set α}
(hs : is_lower_set s) :
is_upper_set (-s)
theorem
is_upper_set.div_left
{α : Type u_1}
[ordered_comm_group α]
{s t : set α}
(ht : is_upper_set t) :
is_lower_set (s / t)
theorem
is_upper_set.sub_left
{α : Type u_1}
[ordered_add_comm_group α]
{s t : set α}
(ht : is_upper_set t) :
is_lower_set (s - t)
theorem
is_upper_set.sub_right
{α : Type u_1}
[ordered_add_comm_group α]
{s t : set α}
(hs : is_upper_set s) :
is_upper_set (s - t)
theorem
is_upper_set.div_right
{α : Type u_1}
[ordered_comm_group α]
{s t : set α}
(hs : is_upper_set s) :
is_upper_set (s / t)
theorem
is_lower_set.div_left
{α : Type u_1}
[ordered_comm_group α]
{s t : set α}
(ht : is_lower_set t) :
is_upper_set (s / t)
theorem
is_lower_set.sub_left
{α : Type u_1}
[ordered_add_comm_group α]
{s t : set α}
(ht : is_lower_set t) :
is_upper_set (s - t)
theorem
is_lower_set.sub_right
{α : Type u_1}
[ordered_add_comm_group α]
{s t : set α}
(hs : is_lower_set s) :
is_lower_set (s - t)
theorem
is_lower_set.div_right
{α : Type u_1}
[ordered_comm_group α]
{s t : set α}
(hs : is_lower_set s) :
is_lower_set (s / t)
@[protected, instance]
Equations
- upper_set.has_one = {one := upper_set.Ici 1}
@[protected, instance]
Equations
@[protected, instance]
Equations
- upper_set.has_add = {add := λ (s t : upper_set α), {carrier := set.image2 has_add.add ↑s ↑t, upper' := _}}
@[protected, instance]
Equations
- upper_set.has_mul = {mul := λ (s t : upper_set α), {carrier := set.image2 has_mul.mul ↑s ↑t, upper' := _}}
@[protected, instance]
Equations
- upper_set.has_div = {div := λ (s t : upper_set α), {carrier := set.image2 has_div.div ↑s ↑t, upper' := _}}
@[protected, instance]
Equations
- upper_set.has_sub = {sub := λ (s t : upper_set α), {carrier := set.image2 has_sub.sub ↑s ↑t, upper' := _}}
@[protected, instance]
@[protected, instance]
@[simp, norm_cast]
@[simp, norm_cast]
@[simp, norm_cast]
@[simp, norm_cast]
@[simp]
@[simp]
@[protected, instance]
Equations
- upper_set.mul_action = function.injective.mul_action coe upper_set.mul_action._proof_1 upper_set.coe_smul
@[protected, instance]
Equations
- upper_set.add_action = function.injective.add_action coe upper_set.add_action._proof_1 upper_set.coe_vadd
@[protected, instance]
Equations
- upper_set.add_comm_semigroup = {add := has_add.add upper_set.has_add, add_assoc := _, add_comm := _}
@[protected, instance]
Equations
- upper_set.comm_semigroup = {mul := has_mul.mul upper_set.has_mul, mul_assoc := _, mul_comm := _}
@[protected, instance]
Equations
- upper_set.comm_monoid = {mul := comm_semigroup.mul upper_set.comm_semigroup, mul_assoc := _, one := 1, one_mul := _, mul_one := _, npow := monoid.npow._default 1 comm_semigroup.mul one_mul upper_set.comm_monoid._proof_3, npow_zero' := _, npow_succ' := _, mul_comm := _}
@[protected, instance]
Equations
- upper_set.add_comm_monoid = {add := add_comm_semigroup.add upper_set.add_comm_semigroup, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := add_monoid.nsmul._default 0 add_comm_semigroup.add _private.205290573.zero_add upper_set.add_comm_monoid._proof_3, nsmul_zero' := _, nsmul_succ' := _, add_comm := _}
@[protected, instance]
Equations
@[protected, instance]
Equations
- lower_set.has_one = {one := lower_set.Iic 1}
@[protected, instance]
Equations
- lower_set.has_add = {add := λ (s t : lower_set α), {carrier := set.image2 has_add.add ↑s ↑t, lower' := _}}
@[protected, instance]
Equations
- lower_set.has_mul = {mul := λ (s t : lower_set α), {carrier := set.image2 has_mul.mul ↑s ↑t, lower' := _}}
@[protected, instance]
Equations
- lower_set.has_div = {div := λ (s t : lower_set α), {carrier := set.image2 has_div.div ↑s ↑t, lower' := _}}
@[protected, instance]
Equations
- lower_set.has_sub = {sub := λ (s t : lower_set α), {carrier := set.image2 has_sub.sub ↑s ↑t, lower' := _}}
@[protected, instance]
@[protected, instance]
@[simp, norm_cast]
@[simp, norm_cast]
@[simp]
@[simp]
@[protected, instance]
Equations
- lower_set.mul_action = function.injective.mul_action coe lower_set.mul_action._proof_1 lower_set.coe_smul
@[protected, instance]
Equations
- lower_set.add_action = function.injective.add_action coe lower_set.add_action._proof_1 lower_set.coe_vadd
@[protected, instance]
Equations
- lower_set.add_comm_semigroup = {add := has_add.add lower_set.has_add, add_assoc := _, add_comm := _}
@[protected, instance]
Equations
- lower_set.comm_semigroup = {mul := has_mul.mul lower_set.has_mul, mul_assoc := _, mul_comm := _}
@[protected, instance]
Equations
- lower_set.add_comm_monoid = {add := add_comm_semigroup.add lower_set.add_comm_semigroup, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := add_monoid.nsmul._default 0 add_comm_semigroup.add _private.1432635499.zero_add lower_set.add_comm_monoid._proof_3, nsmul_zero' := _, nsmul_succ' := _, add_comm := _}
@[protected, instance]
Equations
- lower_set.comm_monoid = {mul := comm_semigroup.mul lower_set.comm_semigroup, mul_assoc := _, one := 1, one_mul := _, mul_one := _, npow := monoid.npow._default 1 comm_semigroup.mul one_mul lower_set.comm_monoid._proof_3, npow_zero' := _, npow_succ' := _, mul_comm := _}
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
theorem
upper_closure_vadd
{α : Type u_1}
[ordered_add_comm_group α]
(s : set α)
(a : α) :
upper_closure (a +ᵥ s) = a +ᵥ upper_closure s
@[simp]
theorem
upper_closure_smul
{α : Type u_1}
[ordered_comm_group α]
(s : set α)
(a : α) :
upper_closure (a • s) = a • upper_closure s
@[simp]
theorem
lower_closure_smul
{α : Type u_1}
[ordered_comm_group α]
(s : set α)
(a : α) :
lower_closure (a • s) = a • lower_closure s
@[simp]
theorem
lower_closure_vadd
{α : Type u_1}
[ordered_add_comm_group α]
(s : set α)
(a : α) :
lower_closure (a +ᵥ s) = a +ᵥ lower_closure s
theorem
mul_upper_closure
{α : Type u_1}
[ordered_comm_group α]
(s t : set α) :
s * ↑(upper_closure t) = ↑(upper_closure (s * t))
theorem
add_upper_closure
{α : Type u_1}
[ordered_add_comm_group α]
(s t : set α) :
s + ↑(upper_closure t) = ↑(upper_closure (s + t))
theorem
mul_lower_closure
{α : Type u_1}
[ordered_comm_group α]
(s t : set α) :
s * ↑(lower_closure t) = ↑(lower_closure (s * t))
theorem
add_lower_closure
{α : Type u_1}
[ordered_add_comm_group α]
(s t : set α) :
s + ↑(lower_closure t) = ↑(lower_closure (s + t))
theorem
upper_closure_add
{α : Type u_1}
[ordered_add_comm_group α]
(s t : set α) :
↑(upper_closure s) + t = ↑(upper_closure (s + t))
theorem
upper_closure_mul
{α : Type u_1}
[ordered_comm_group α]
(s t : set α) :
↑(upper_closure s) * t = ↑(upper_closure (s * t))
theorem
lower_closure_add
{α : Type u_1}
[ordered_add_comm_group α]
(s t : set α) :
↑(lower_closure s) + t = ↑(lower_closure (s + t))
theorem
lower_closure_mul
{α : Type u_1}
[ordered_comm_group α]
(s t : set α) :
↑(lower_closure s) * t = ↑(lower_closure (s * t))
@[simp]
theorem
upper_closure_add_distrib
{α : Type u_1}
[ordered_add_comm_group α]
(s t : set α) :
upper_closure (s + t) = upper_closure s + upper_closure t
@[simp]
theorem
upper_closure_mul_distrib
{α : Type u_1}
[ordered_comm_group α]
(s t : set α) :
upper_closure (s * t) = upper_closure s * upper_closure t
@[simp]
theorem
lower_closure_mul_distrib
{α : Type u_1}
[ordered_comm_group α]
(s t : set α) :
lower_closure (s * t) = lower_closure s * lower_closure t
@[simp]
theorem
lower_closure_add_distrib
{α : Type u_1}
[ordered_add_comm_group α]
(s t : set α) :
lower_closure (s + t) = lower_closure s + lower_closure t