Documentation

Mathlib.Algebra.Order.UpperLower

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} [OrderedAddCommMonoid α] {s : Set α} {x : α} (hs : IsUpperSet s) (hx : 0 x) :
x +ᵥ s s
theorem IsUpperSet.smul_subset {α : Type u_1} [OrderedCommMonoid α] {s : Set α} {x : α} (hs : IsUpperSet s) (hx : 1 x) :
x s s
theorem IsLowerSet.vadd_subset {α : Type u_1} [OrderedAddCommMonoid α] {s : Set α} {x : α} (hs : IsLowerSet s) (hx : x 0) :
x +ᵥ s s
theorem IsLowerSet.smul_subset {α : Type u_1} [OrderedCommMonoid α] {s : Set α} {x : α} (hs : IsLowerSet s) (hx : x 1) :
x s s
theorem IsUpperSet.vadd {α : Type u_1} [OrderedAddCommGroup α] {s : Set α} {a : α} (hs : IsUpperSet s) :
theorem IsUpperSet.smul {α : Type u_1} [OrderedCommGroup α] {s : Set α} {a : α} (hs : IsUpperSet s) :
theorem IsLowerSet.vadd {α : Type u_1} [OrderedAddCommGroup α] {s : Set α} {a : α} (hs : IsLowerSet s) :
theorem IsLowerSet.smul {α : Type u_1} [OrderedCommGroup α] {s : Set α} {a : α} (hs : IsLowerSet s) :
theorem Set.OrdConnected.vadd {α : Type u_1} [OrderedAddCommGroup α] {s : Set α} {a : α} (hs : s.OrdConnected) :
(a +ᵥ s).OrdConnected
theorem Set.OrdConnected.smul {α : Type u_1} [OrderedCommGroup α] {s : Set α} {a : α} (hs : s.OrdConnected) :
(a s).OrdConnected
theorem IsUpperSet.add_left {α : Type u_1} [OrderedAddCommGroup α] {s : Set α} {t : Set α} (ht : IsUpperSet t) :
theorem IsUpperSet.mul_left {α : Type u_1} [OrderedCommGroup α] {s : Set α} {t : Set α} (ht : IsUpperSet t) :
theorem IsUpperSet.add_right {α : Type u_1} [OrderedAddCommGroup α] {s : Set α} {t : Set α} (hs : IsUpperSet s) :
theorem IsUpperSet.mul_right {α : Type u_1} [OrderedCommGroup α] {s : Set α} {t : Set α} (hs : IsUpperSet s) :
theorem IsLowerSet.add_left {α : Type u_1} [OrderedAddCommGroup α] {s : Set α} {t : Set α} (ht : IsLowerSet t) :
theorem IsLowerSet.mul_left {α : Type u_1} [OrderedCommGroup α] {s : Set α} {t : Set α} (ht : IsLowerSet t) :
theorem IsLowerSet.add_right {α : Type u_1} [OrderedAddCommGroup α] {s : Set α} {t : Set α} (hs : IsLowerSet s) :
theorem IsLowerSet.mul_right {α : Type u_1} [OrderedCommGroup α] {s : Set α} {t : Set α} (hs : IsLowerSet s) :
theorem IsUpperSet.neg {α : Type u_1} [OrderedAddCommGroup α] {s : Set α} (hs : IsUpperSet s) :
theorem IsUpperSet.inv {α : Type u_1} [OrderedCommGroup α] {s : Set α} (hs : IsUpperSet s) :
theorem IsLowerSet.neg {α : Type u_1} [OrderedAddCommGroup α] {s : Set α} (hs : IsLowerSet s) :
theorem IsLowerSet.inv {α : Type u_1} [OrderedCommGroup α] {s : Set α} (hs : IsLowerSet s) :
theorem IsUpperSet.sub_left {α : Type u_1} [OrderedAddCommGroup α] {s : Set α} {t : Set α} (ht : IsUpperSet t) :
theorem IsUpperSet.div_left {α : Type u_1} [OrderedCommGroup α] {s : Set α} {t : Set α} (ht : IsUpperSet t) :
theorem IsUpperSet.sub_right {α : Type u_1} [OrderedAddCommGroup α] {s : Set α} {t : Set α} (hs : IsUpperSet s) :
theorem IsUpperSet.div_right {α : Type u_1} [OrderedCommGroup α] {s : Set α} {t : Set α} (hs : IsUpperSet s) :
theorem IsLowerSet.sub_left {α : Type u_1} [OrderedAddCommGroup α] {s : Set α} {t : Set α} (ht : IsLowerSet t) :
theorem IsLowerSet.div_left {α : Type u_1} [OrderedCommGroup α] {s : Set α} {t : Set α} (ht : IsLowerSet t) :
theorem IsLowerSet.sub_right {α : Type u_1} [OrderedAddCommGroup α] {s : Set α} {t : Set α} (hs : IsLowerSet s) :
theorem IsLowerSet.div_right {α : Type u_1} [OrderedCommGroup α] {s : Set α} {t : Set α} (hs : IsLowerSet s) :
instance UpperSet.instZero {α : Type u_1} [OrderedAddCommGroup α] :
Equations
instance UpperSet.instOne {α : Type u_1} [OrderedCommGroup α] :
Equations
instance UpperSet.instAdd {α : Type u_1} [OrderedAddCommGroup α] :
Equations
  • UpperSet.instAdd = { add := fun (s t : UpperSet α) => { carrier := Set.image2 (fun (x1 x2 : α) => x1 + x2) s t, upper' := } }
instance UpperSet.instMul {α : Type u_1} [OrderedCommGroup α] :
Equations
  • UpperSet.instMul = { mul := fun (s t : UpperSet α) => { carrier := Set.image2 (fun (x1 x2 : α) => x1 * x2) s t, upper' := } }
instance UpperSet.instSub {α : Type u_1} [OrderedAddCommGroup α] :
Equations
  • UpperSet.instSub = { sub := fun (s t : UpperSet α) => { carrier := Set.image2 (fun (x1 x2 : α) => x1 - x2) s t, upper' := } }
instance UpperSet.instDiv {α : Type u_1} [OrderedCommGroup α] :
Equations
  • UpperSet.instDiv = { div := fun (s t : UpperSet α) => { carrier := Set.image2 (fun (x1 x2 : α) => x1 / x2) s t, upper' := } }
instance UpperSet.instVAdd {α : Type u_1} [OrderedAddCommGroup α] :
VAdd α (UpperSet α)
Equations
  • UpperSet.instVAdd = { vadd := fun (a : α) (s : UpperSet α) => { carrier := (fun (x : α) => a +ᵥ x) '' s, upper' := } }
instance UpperSet.instSMul {α : Type u_1} [OrderedCommGroup α] :
SMul α (UpperSet α)
Equations
  • UpperSet.instSMul = { smul := fun (a : α) (s : UpperSet α) => { carrier := (fun (x : α) => a x) '' s, upper' := } }
@[simp]
theorem UpperSet.coe_zero {α : Type u_1} [OrderedAddCommGroup α] :
0 = Set.Ici 0
@[simp]
theorem UpperSet.coe_one {α : Type u_1} [OrderedCommGroup α] :
1 = Set.Ici 1
@[simp]
theorem UpperSet.coe_add {α : Type u_1} [OrderedAddCommGroup α] (s : UpperSet α) (t : UpperSet α) :
(s + t) = s + t
@[simp]
theorem UpperSet.coe_mul {α : Type u_1} [OrderedCommGroup α] (s : UpperSet α) (t : UpperSet α) :
(s * t) = s * t
@[simp]
theorem UpperSet.coe_sub {α : Type u_1} [OrderedAddCommGroup α] (s : UpperSet α) (t : UpperSet α) :
(s - t) = s - t
@[simp]
theorem UpperSet.coe_div {α : Type u_1} [OrderedCommGroup α] (s : UpperSet α) (t : UpperSet α) :
(s / t) = s / t
@[simp]
@[simp]
theorem UpperSet.Ici_one {α : Type u_1} [OrderedCommGroup α] :
Equations
Equations
Equations
Equations
Equations
Equations
instance LowerSet.instZero {α : Type u_1} [OrderedAddCommGroup α] :
Equations
instance LowerSet.instOne {α : Type u_1} [OrderedCommGroup α] :
Equations
instance LowerSet.instAdd {α : Type u_1} [OrderedAddCommGroup α] :
Equations
  • LowerSet.instAdd = { add := fun (s t : LowerSet α) => { carrier := Set.image2 (fun (x1 x2 : α) => x1 + x2) s t, lower' := } }
instance LowerSet.instMul {α : Type u_1} [OrderedCommGroup α] :
Equations
  • LowerSet.instMul = { mul := fun (s t : LowerSet α) => { carrier := Set.image2 (fun (x1 x2 : α) => x1 * x2) s t, lower' := } }
instance LowerSet.instSub {α : Type u_1} [OrderedAddCommGroup α] :
Equations
  • LowerSet.instSub = { sub := fun (s t : LowerSet α) => { carrier := Set.image2 (fun (x1 x2 : α) => x1 - x2) s t, lower' := } }
instance LowerSet.instDiv {α : Type u_1} [OrderedCommGroup α] :
Equations
  • LowerSet.instDiv = { div := fun (s t : LowerSet α) => { carrier := Set.image2 (fun (x1 x2 : α) => x1 / x2) s t, lower' := } }
instance LowerSet.instVAdd {α : Type u_1} [OrderedAddCommGroup α] :
VAdd α (LowerSet α)
Equations
  • LowerSet.instVAdd = { vadd := fun (a : α) (s : LowerSet α) => { carrier := (fun (x : α) => a +ᵥ x) '' s, lower' := } }
instance LowerSet.instSMul {α : Type u_1} [OrderedCommGroup α] :
SMul α (LowerSet α)
Equations
  • LowerSet.instSMul = { smul := fun (a : α) (s : LowerSet α) => { carrier := (fun (x : α) => a x) '' s, lower' := } }
@[simp]
theorem LowerSet.coe_add {α : Type u_1} [OrderedAddCommGroup α] (s : LowerSet α) (t : LowerSet α) :
(s + t) = s + t
@[simp]
theorem LowerSet.coe_mul {α : Type u_1} [OrderedCommGroup α] (s : LowerSet α) (t : LowerSet α) :
(s * t) = s * t
@[simp]
theorem LowerSet.coe_sub {α : Type u_1} [OrderedAddCommGroup α] (s : LowerSet α) (t : LowerSet α) :
(s - t) = s - t
@[simp]
theorem LowerSet.coe_div {α : Type u_1} [OrderedCommGroup α] (s : LowerSet α) (t : LowerSet α) :
(s / t) = s / t
@[simp]
@[simp]
theorem LowerSet.Iic_one {α : Type u_1} [OrderedCommGroup α] :
Equations
Equations
Equations
Equations
Equations
Equations
@[simp]
@[simp]
theorem upperClosure_one {α : Type u_1} [OrderedCommGroup α] :
@[simp]
@[simp]
theorem lowerClosure_one {α : Type u_1} [OrderedCommGroup α] :
@[simp]
theorem upperClosure_vadd {α : Type u_1} [OrderedAddCommGroup α] (s : Set α) (a : α) :
@[simp]
theorem upperClosure_smul {α : Type u_1} [OrderedCommGroup α] (s : Set α) (a : α) :
@[simp]
theorem lowerClosure_vadd {α : Type u_1} [OrderedAddCommGroup α] (s : Set α) (a : α) :
@[simp]
theorem lowerClosure_smul {α : Type u_1} [OrderedCommGroup α] (s : Set α) (a : α) :
theorem add_upperClosure {α : Type u_1} [OrderedAddCommGroup α] (s : Set α) (t : Set α) :
s + (upperClosure t) = (upperClosure (s + t))
theorem mul_upperClosure {α : Type u_1} [OrderedCommGroup α] (s : Set α) (t : Set α) :
s * (upperClosure t) = (upperClosure (s * t))
theorem add_lowerClosure {α : Type u_1} [OrderedAddCommGroup α] (s : Set α) (t : Set α) :
s + (lowerClosure t) = (lowerClosure (s + t))
theorem mul_lowerClosure {α : Type u_1} [OrderedCommGroup α] (s : Set α) (t : Set α) :
s * (lowerClosure t) = (lowerClosure (s * t))
theorem upperClosure_add {α : Type u_1} [OrderedAddCommGroup α] (s : Set α) (t : Set α) :
(upperClosure s) + t = (upperClosure (s + t))
theorem upperClosure_mul {α : Type u_1} [OrderedCommGroup α] (s : Set α) (t : Set α) :
(upperClosure s) * t = (upperClosure (s * t))
theorem lowerClosure_add {α : Type u_1} [OrderedAddCommGroup α] (s : Set α) (t : Set α) :
(lowerClosure s) + t = (lowerClosure (s + t))
theorem lowerClosure_mul {α : Type u_1} [OrderedCommGroup α] (s : Set α) (t : Set α) :
(lowerClosure s) * t = (lowerClosure (s * t))
@[simp]
theorem upperClosure_add_distrib {α : Type u_1} [OrderedAddCommGroup α] (s : Set α) (t : Set α) :
@[simp]
theorem upperClosure_mul_distrib {α : Type u_1} [OrderedCommGroup α] (s : Set α) (t : Set α) :
@[simp]
theorem lowerClosure_add_distrib {α : Type u_1} [OrderedAddCommGroup α] (s : Set α) (t : Set α) :
@[simp]
theorem lowerClosure_mul_distrib {α : Type u_1} [OrderedCommGroup α] (s : Set α) (t : Set α) :