# Algebraic operations on upper/lower sets #

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

theorem IsUpperSet.vadd_subset {α : Type u_1} {s : Set α} {x : α} (hs : ) (hx : 0 x) :
x +ᵥ s s
theorem IsUpperSet.smul_subset {α : Type u_1} {s : Set α} {x : α} (hs : ) (hx : 1 x) :
x s s
theorem IsLowerSet.vadd_subset {α : Type u_1} {s : Set α} {x : α} (hs : ) (hx : x 0) :
x +ᵥ s s
theorem IsLowerSet.smul_subset {α : Type u_1} {s : Set α} {x : α} (hs : ) (hx : x 1) :
x s s
theorem IsUpperSet.vadd {α : Type u_1} {s : Set α} {a : α} (hs : ) :
theorem IsUpperSet.smul {α : Type u_1} [] {s : Set α} {a : α} (hs : ) :
theorem IsLowerSet.vadd {α : Type u_1} {s : Set α} {a : α} (hs : ) :
theorem IsLowerSet.smul {α : Type u_1} [] {s : Set α} {a : α} (hs : ) :
theorem Set.OrdConnected.vadd {α : Type u_1} {s : Set α} {a : α} (hs : s.OrdConnected) :
(a +ᵥ s).OrdConnected
theorem Set.OrdConnected.smul {α : Type u_1} [] {s : Set α} {a : α} (hs : s.OrdConnected) :
(a s).OrdConnected
theorem IsUpperSet.add_left {α : Type u_1} {s : Set α} {t : Set α} (ht : ) :
theorem IsUpperSet.mul_left {α : Type u_1} [] {s : Set α} {t : Set α} (ht : ) :
theorem IsUpperSet.add_right {α : Type u_1} {s : Set α} {t : Set α} (hs : ) :
theorem IsUpperSet.mul_right {α : Type u_1} [] {s : Set α} {t : Set α} (hs : ) :
theorem IsLowerSet.add_left {α : Type u_1} {s : Set α} {t : Set α} (ht : ) :
theorem IsLowerSet.mul_left {α : Type u_1} [] {s : Set α} {t : Set α} (ht : ) :
theorem IsLowerSet.add_right {α : Type u_1} {s : Set α} {t : Set α} (hs : ) :
theorem IsLowerSet.mul_right {α : Type u_1} [] {s : Set α} {t : Set α} (hs : ) :
theorem IsUpperSet.neg {α : Type u_1} {s : Set α} (hs : ) :
theorem IsUpperSet.inv {α : Type u_1} [] {s : Set α} (hs : ) :
theorem IsLowerSet.neg {α : Type u_1} {s : Set α} (hs : ) :
theorem IsLowerSet.inv {α : Type u_1} [] {s : Set α} (hs : ) :
theorem IsUpperSet.sub_left {α : Type u_1} {s : Set α} {t : Set α} (ht : ) :
theorem IsUpperSet.div_left {α : Type u_1} [] {s : Set α} {t : Set α} (ht : ) :
theorem IsUpperSet.sub_right {α : Type u_1} {s : Set α} {t : Set α} (hs : ) :
theorem IsUpperSet.div_right {α : Type u_1} [] {s : Set α} {t : Set α} (hs : ) :
theorem IsLowerSet.sub_left {α : Type u_1} {s : Set α} {t : Set α} (ht : ) :
theorem IsLowerSet.div_left {α : Type u_1} [] {s : Set α} {t : Set α} (ht : ) :
theorem IsLowerSet.sub_right {α : Type u_1} {s : Set α} {t : Set α} (hs : ) :
theorem IsLowerSet.div_right {α : Type u_1} [] {s : Set α} {t : Set α} (hs : ) :
instance UpperSet.instZero {α : Type u_1} :
Zero ()
Equations
• UpperSet.instZero = { zero := }
instance UpperSet.instOne {α : Type u_1} [] :
One ()
Equations
• UpperSet.instOne = { one := }
theorem UpperSet.instAdd.proof_1 {α : Type u_1} (s : ) (t : ) :
IsUpperSet (s.carrier + t)
instance UpperSet.instAdd {α : Type u_1} :
Equations
• UpperSet.instAdd = { add := fun (s t : ) => { carrier := Set.image2 (fun (x x_1 : α) => x + x_1) s t, upper' := } }
instance UpperSet.instMul {α : Type u_1} [] :
Mul ()
Equations
• UpperSet.instMul = { mul := fun (s t : ) => { carrier := Set.image2 (fun (x x_1 : α) => x * x_1) s t, upper' := } }
instance UpperSet.instSub {α : Type u_1} :
Sub ()
Equations
• UpperSet.instSub = { sub := fun (s t : ) => { carrier := Set.image2 (fun (x x_1 : α) => x - x_1) s t, upper' := } }
theorem UpperSet.instSub.proof_1 {α : Type u_1} (s : ) (t : ) :
IsUpperSet (s.carrier - t)
instance UpperSet.instDiv {α : Type u_1} [] :
Div ()
Equations
• UpperSet.instDiv = { div := fun (s t : ) => { carrier := Set.image2 (fun (x x_1 : α) => x / x_1) s t, upper' := } }
instance UpperSet.instVAdd {α : Type u_1} :
Equations
• UpperSet.instVAdd = { vadd := fun (a : α) (s : ) => { carrier := (fun (x : α) => a +ᵥ x) '' s, upper' := } }
theorem UpperSet.instVAdd.proof_1 {α : Type u_1} (a : α) (s : ) :
IsUpperSet (a +ᵥ s.carrier)
instance UpperSet.instSMul {α : Type u_1} [] :
SMul α ()
Equations
• UpperSet.instSMul = { smul := fun (a : α) (s : ) => { carrier := (fun (x : α) => a x) '' s, upper' := } }
@[simp]
theorem UpperSet.coe_zero {α : Type u_1} :
0 =
@[simp]
theorem UpperSet.coe_one {α : Type u_1} [] :
1 =
@[simp]
theorem UpperSet.coe_add {α : Type u_1} (s : ) (t : ) :
(s + t) = s + t
@[simp]
theorem UpperSet.coe_mul {α : Type u_1} [] (s : ) (t : ) :
(s * t) = s * t
@[simp]
theorem UpperSet.coe_sub {α : Type u_1} (s : ) (t : ) :
(s - t) = s - t
@[simp]
theorem UpperSet.coe_div {α : Type u_1} [] (s : ) (t : ) :
(s / t) = s / t
@[simp]
theorem UpperSet.Ici_zero {α : Type u_1} :
@[simp]
theorem UpperSet.Ici_one {α : Type u_1} [] :
instance UpperSet.instAddAction {α : Type u_1} :
Equations
theorem UpperSet.instAddAction.proof_2 {α : Type u_1} :
∀ (x : α) (x_1 : ), (x +ᵥ x_1) = (x +ᵥ x_1)
instance UpperSet.instMulAction {α : Type u_1} [] :
MulAction α ()
Equations
theorem UpperSet.addCommSemigroup.proof_2 {α : Type u_1} (a : ) (b : ) :
a + b = b + a
instance UpperSet.addCommSemigroup {α : Type u_1} :
Equations
instance UpperSet.commSemigroup {α : Type u_1} [] :
Equations
theorem UpperSet.instAddCommMonoid.proof_2 {α : Type u_1} :
∀ (x : ), nsmulRec 0 x = nsmulRec 0 x
instance UpperSet.instAddCommMonoid {α : Type u_1} :
Equations
• UpperSet.instAddCommMonoid = let __src := UpperSet.addCommSemigroup;
theorem UpperSet.instAddCommMonoid.proof_4 {α : Type u_1} (a : ) (b : ) :
a + b = b + a
theorem UpperSet.instAddCommMonoid.proof_1 {α : Type u_1} (s : ) :
s + 0 = s
theorem UpperSet.instAddCommMonoid.proof_3 {α : Type u_1} :
∀ (n : ) (x : ), nsmulRec (n + 1) x = nsmulRec (n + 1) x
instance UpperSet.instCommMonoid {α : Type u_1} [] :
Equations
• UpperSet.instCommMonoid = let __src := UpperSet.commSemigroup;
instance LowerSet.instZero {α : Type u_1} :
Zero ()
Equations
• LowerSet.instZero = { zero := }
instance LowerSet.instOne {α : Type u_1} [] :
One ()
Equations
• LowerSet.instOne = { one := }
instance LowerSet.instAdd {α : Type u_1} :
Equations
• LowerSet.instAdd = { add := fun (s t : ) => { carrier := Set.image2 (fun (x x_1 : α) => x + x_1) s t, lower' := } }
theorem LowerSet.instAdd.proof_1 {α : Type u_1} (s : ) (t : ) :
IsLowerSet (s.carrier + t)
instance LowerSet.instMul {α : Type u_1} [] :
Mul ()
Equations
• LowerSet.instMul = { mul := fun (s t : ) => { carrier := Set.image2 (fun (x x_1 : α) => x * x_1) s t, lower' := } }
instance LowerSet.instSub {α : Type u_1} :
Sub ()
Equations
• LowerSet.instSub = { sub := fun (s t : ) => { carrier := Set.image2 (fun (x x_1 : α) => x - x_1) s t, lower' := } }
theorem LowerSet.instSub.proof_1 {α : Type u_1} (s : ) (t : ) :
IsLowerSet (s.carrier - t)
instance LowerSet.instDiv {α : Type u_1} [] :
Div ()
Equations
• LowerSet.instDiv = { div := fun (s t : ) => { carrier := Set.image2 (fun (x x_1 : α) => x / x_1) s t, lower' := } }
instance LowerSet.instVAdd {α : Type u_1} :
Equations
• LowerSet.instVAdd = { vadd := fun (a : α) (s : ) => { carrier := (fun (x : α) => a +ᵥ x) '' s, lower' := } }
theorem LowerSet.instVAdd.proof_1 {α : Type u_1} (a : α) (s : ) :
IsLowerSet (a +ᵥ s.carrier)
instance LowerSet.instSMul {α : Type u_1} [] :
SMul α ()
Equations
• LowerSet.instSMul = { smul := fun (a : α) (s : ) => { carrier := (fun (x : α) => a x) '' s, lower' := } }
@[simp]
theorem LowerSet.coe_add {α : Type u_1} (s : ) (t : ) :
(s + t) = s + t
@[simp]
theorem LowerSet.coe_mul {α : Type u_1} [] (s : ) (t : ) :
(s * t) = s * t
@[simp]
theorem LowerSet.coe_sub {α : Type u_1} (s : ) (t : ) :
(s - t) = s - t
@[simp]
theorem LowerSet.coe_div {α : Type u_1} [] (s : ) (t : ) :
(s / t) = s / t
@[simp]
theorem LowerSet.Iic_zero {α : Type u_1} :
@[simp]
theorem LowerSet.Iic_one {α : Type u_1} [] :
theorem LowerSet.instAddAction.proof_2 {α : Type u_1} :
∀ (x : α) (x_1 : ), (x +ᵥ x_1) = (x +ᵥ x_1)
instance LowerSet.instAddAction {α : Type u_1} :
Equations
instance LowerSet.instMulAction {α : Type u_1} [] :
MulAction α ()
Equations
instance LowerSet.addCommSemigroup {α : Type u_1} :
Equations
theorem LowerSet.addCommSemigroup.proof_2 {α : Type u_1} (a : ) (b : ) :
a + b = b + a
instance LowerSet.commSemigroup {α : Type u_1} [] :
Equations
instance LowerSet.instAddCommMonoid {α : Type u_1} :
Equations
• LowerSet.instAddCommMonoid = let __src := LowerSet.addCommSemigroup;
theorem LowerSet.instAddCommMonoid.proof_3 {α : Type u_1} :
∀ (n : ) (x : ), nsmulRec (n + 1) x = nsmulRec (n + 1) x
theorem LowerSet.instAddCommMonoid.proof_1 {α : Type u_1} (s : ) :
s + 0 = s
theorem LowerSet.instAddCommMonoid.proof_4 {α : Type u_1} (a : ) (b : ) :
a + b = b + a
theorem LowerSet.instAddCommMonoid.proof_2 {α : Type u_1} :
∀ (x : ), nsmulRec 0 x = nsmulRec 0 x
instance LowerSet.instCommMonoid {α : Type u_1} [] :
Equations
• LowerSet.instCommMonoid = let __src := LowerSet.commSemigroup;
@[simp]
theorem upperClosure_zero {α : Type u_1} :
@[simp]
theorem upperClosure_one {α : Type u_1} [] :
@[simp]
theorem lowerClosure_zero {α : Type u_1} :
@[simp]
theorem lowerClosure_one {α : Type u_1} [] :
@[simp]
theorem upperClosure_vadd {α : Type u_1} (s : Set α) (a : α) :
@[simp]
theorem upperClosure_smul {α : Type u_1} [] (s : Set α) (a : α) :
@[simp]
theorem lowerClosure_vadd {α : Type u_1} (s : Set α) (a : α) :
@[simp]
theorem lowerClosure_smul {α : Type u_1} [] (s : Set α) (a : α) :
theorem add_upperClosure {α : Type u_1} (s : Set α) (t : Set α) :
s + () = (upperClosure (s + t))
theorem mul_upperClosure {α : Type u_1} [] (s : Set α) (t : Set α) :
s * () = (upperClosure (s * t))
theorem add_lowerClosure {α : Type u_1} (s : Set α) (t : Set α) :
s + () = (lowerClosure (s + t))
theorem mul_lowerClosure {α : Type u_1} [] (s : Set α) (t : Set α) :
s * () = (lowerClosure (s * t))
theorem upperClosure_add {α : Type u_1} (s : Set α) (t : Set α) :
() + t = (upperClosure (s + t))
theorem upperClosure_mul {α : Type u_1} [] (s : Set α) (t : Set α) :
() * t = (upperClosure (s * t))
theorem lowerClosure_add {α : Type u_1} (s : Set α) (t : Set α) :
() + t = (lowerClosure (s + t))
theorem lowerClosure_mul {α : Type u_1} [] (s : Set α) (t : Set α) :
() * t = (lowerClosure (s * t))
@[simp]
theorem upperClosure_add_distrib {α : Type u_1} (s : Set α) (t : Set α) :
@[simp]
theorem upperClosure_mul_distrib {α : Type u_1} [] (s : Set α) (t : Set α) :
@[simp]
theorem lowerClosure_add_distrib {α : Type u_1} (s : Set α) (t : Set α) :
@[simp]
theorem lowerClosure_mul_distrib {α : Type u_1} [] (s : Set α) (t : Set α) :