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)
:
theorem
IsUpperSet.smul_subset
{α : Type u_1}
[OrderedCommMonoid α]
{s : Set α}
{x : α}
(hs : IsUpperSet s)
(hx : 1 ≤ x)
:
theorem
IsLowerSet.vadd_subset
{α : Type u_1}
[OrderedAddCommMonoid α]
{s : Set α}
{x : α}
(hs : IsLowerSet s)
(hx : x ≤ 0)
:
theorem
IsLowerSet.smul_subset
{α : Type u_1}
[OrderedCommMonoid α]
{s : Set α}
{x : α}
(hs : IsLowerSet s)
(hx : x ≤ 1)
:
theorem
IsUpperSet.vadd
{α : Type u_1}
[OrderedAddCommGroup α]
{s : Set α}
{a : α}
(hs : IsUpperSet s)
:
IsUpperSet (a +ᵥ s)
theorem
IsUpperSet.smul
{α : Type u_1}
[OrderedCommGroup α]
{s : Set α}
{a : α}
(hs : IsUpperSet s)
:
IsUpperSet (a • s)
theorem
IsLowerSet.vadd
{α : Type u_1}
[OrderedAddCommGroup α]
{s : Set α}
{a : α}
(hs : IsLowerSet s)
:
IsLowerSet (a +ᵥ s)
theorem
IsLowerSet.smul
{α : Type u_1}
[OrderedCommGroup α]
{s : Set α}
{a : α}
(hs : IsLowerSet s)
:
IsLowerSet (a • s)
theorem
Set.OrdConnected.vadd
{α : Type u_1}
[OrderedAddCommGroup α]
{s : Set α}
{a : α}
(hs : Set.OrdConnected s)
:
Set.OrdConnected (a +ᵥ s)
theorem
Set.OrdConnected.smul
{α : Type u_1}
[OrderedCommGroup α]
{s : Set α}
{a : α}
(hs : Set.OrdConnected s)
:
Set.OrdConnected (a • s)
theorem
IsUpperSet.add_left
{α : Type u_1}
[OrderedAddCommGroup α]
{s : Set α}
{t : Set α}
(ht : IsUpperSet t)
:
IsUpperSet (s + t)
theorem
IsUpperSet.mul_left
{α : Type u_1}
[OrderedCommGroup α]
{s : Set α}
{t : Set α}
(ht : IsUpperSet t)
:
IsUpperSet (s * t)
theorem
IsUpperSet.add_right
{α : Type u_1}
[OrderedAddCommGroup α]
{s : Set α}
{t : Set α}
(hs : IsUpperSet s)
:
IsUpperSet (s + t)
theorem
IsUpperSet.mul_right
{α : Type u_1}
[OrderedCommGroup α]
{s : Set α}
{t : Set α}
(hs : IsUpperSet s)
:
IsUpperSet (s * t)
theorem
IsLowerSet.add_left
{α : Type u_1}
[OrderedAddCommGroup α]
{s : Set α}
{t : Set α}
(ht : IsLowerSet t)
:
IsLowerSet (s + t)
theorem
IsLowerSet.mul_left
{α : Type u_1}
[OrderedCommGroup α]
{s : Set α}
{t : Set α}
(ht : IsLowerSet t)
:
IsLowerSet (s * t)
theorem
IsLowerSet.add_right
{α : Type u_1}
[OrderedAddCommGroup α]
{s : Set α}
{t : Set α}
(hs : IsLowerSet s)
:
IsLowerSet (s + t)
theorem
IsLowerSet.mul_right
{α : Type u_1}
[OrderedCommGroup α]
{s : Set α}
{t : Set α}
(hs : IsLowerSet s)
:
IsLowerSet (s * t)
theorem
IsUpperSet.neg
{α : Type u_1}
[OrderedAddCommGroup α]
{s : Set α}
(hs : IsUpperSet s)
:
IsLowerSet (-s)
theorem
IsLowerSet.neg
{α : Type u_1}
[OrderedAddCommGroup α]
{s : Set α}
(hs : IsLowerSet s)
:
IsUpperSet (-s)
theorem
IsUpperSet.sub_left
{α : Type u_1}
[OrderedAddCommGroup α]
{s : Set α}
{t : Set α}
(ht : IsUpperSet t)
:
IsLowerSet (s - t)
theorem
IsUpperSet.div_left
{α : Type u_1}
[OrderedCommGroup α]
{s : Set α}
{t : Set α}
(ht : IsUpperSet t)
:
IsLowerSet (s / t)
theorem
IsUpperSet.sub_right
{α : Type u_1}
[OrderedAddCommGroup α]
{s : Set α}
{t : Set α}
(hs : IsUpperSet s)
:
IsUpperSet (s - t)
theorem
IsUpperSet.div_right
{α : Type u_1}
[OrderedCommGroup α]
{s : Set α}
{t : Set α}
(hs : IsUpperSet s)
:
IsUpperSet (s / t)
theorem
IsLowerSet.sub_left
{α : Type u_1}
[OrderedAddCommGroup α]
{s : Set α}
{t : Set α}
(ht : IsLowerSet t)
:
IsUpperSet (s - t)
theorem
IsLowerSet.div_left
{α : Type u_1}
[OrderedCommGroup α]
{s : Set α}
{t : Set α}
(ht : IsLowerSet t)
:
IsUpperSet (s / t)
theorem
IsLowerSet.sub_right
{α : Type u_1}
[OrderedAddCommGroup α]
{s : Set α}
{t : Set α}
(hs : IsLowerSet s)
:
IsLowerSet (s - t)
theorem
IsLowerSet.div_right
{α : Type u_1}
[OrderedCommGroup α]
{s : Set α}
{t : Set α}
(hs : IsLowerSet s)
:
IsLowerSet (s / t)
instance
UpperSet.instZeroUpperSetToLEToPreorderToPartialOrder
{α : Type u_1}
[OrderedAddCommGroup α]
:
Equations
- UpperSet.instZeroUpperSetToLEToPreorderToPartialOrder = { zero := UpperSet.Ici 0 }
Equations
- UpperSet.instOneUpperSetToLEToPreorderToPartialOrder = { one := UpperSet.Ici 1 }
instance
UpperSet.instAddUpperSetToLEToPreorderToPartialOrder
{α : Type u_1}
[OrderedAddCommGroup α]
:
Equations
- One or more equations did not get rendered due to their size.
theorem
UpperSet.instAddUpperSetToLEToPreorderToPartialOrder.proof_1
{α : Type u_1}
[OrderedAddCommGroup α]
(s : UpperSet α)
(t : UpperSet α)
:
IsUpperSet (s.carrier + ↑t)
Equations
- One or more equations did not get rendered due to their size.
theorem
UpperSet.instSubUpperSetToLEToPreorderToPartialOrder.proof_1
{α : Type u_1}
[OrderedAddCommGroup α]
(s : UpperSet α)
(t : UpperSet α)
:
IsUpperSet (s.carrier - ↑t)
instance
UpperSet.instSubUpperSetToLEToPreorderToPartialOrder
{α : Type u_1}
[OrderedAddCommGroup α]
:
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
instance
UpperSet.instVAddUpperSetToLEToPreorderToPartialOrder
{α : Type u_1}
[OrderedAddCommGroup α]
:
Equations
- One or more equations did not get rendered due to their size.
theorem
UpperSet.instVAddUpperSetToLEToPreorderToPartialOrder.proof_1
{α : Type u_1}
[OrderedAddCommGroup α]
(a : α)
(s : UpperSet α)
:
IsUpperSet (a +ᵥ s.carrier)
instance
UpperSet.instSMulUpperSetToLEToPreorderToPartialOrder
{α : Type u_1}
[OrderedCommGroup α]
:
Equations
- One or more equations did not get rendered due to their size.
@[simp]
@[simp]
@[simp]
@[simp]
instance
UpperSet.instAddActionUpperSetToLEToPreorderToPartialOrderToAddMonoidToSubNegAddMonoidToAddGroupToAddCommGroup
{α : Type u_1}
[OrderedAddCommGroup α]
:
Equations
- One or more equations did not get rendered due to their size.
instance
UpperSet.instMulActionUpperSetToLEToPreorderToPartialOrderToMonoidToDivInvMonoidToGroupToCommGroup
{α : Type u_1}
[OrderedCommGroup α]
:
Equations
- One or more equations did not get rendered due to their size.
theorem
UpperSet.addCommSemigroup.proof_1
{α : Type u_1}
[OrderedAddCommGroup α]
:
Function.Injective SetLike.coe
Equations
- One or more equations did not get rendered due to their size.
theorem
UpperSet.addCommSemigroup.proof_2
{α : Type u_1}
[OrderedAddCommGroup α]
(a : UpperSet α)
(b : UpperSet α)
:
Equations
- One or more equations did not get rendered due to their size.
theorem
UpperSet.instAddCommMonoidUpperSetToLEToPreorderToPartialOrder.proof_4
{α : Type u_1}
[OrderedAddCommGroup α]
(a : UpperSet α)
(b : UpperSet α)
:
theorem
UpperSet.instAddCommMonoidUpperSetToLEToPreorderToPartialOrder.proof_2
{α : Type u_1}
[OrderedAddCommGroup α]
:
theorem
UpperSet.instAddCommMonoidUpperSetToLEToPreorderToPartialOrder.proof_3
{α : Type u_1}
[OrderedAddCommGroup α]
:
instance
UpperSet.instAddCommMonoidUpperSetToLEToPreorderToPartialOrder
{α : Type u_1}
[OrderedAddCommGroup α]
:
theorem
UpperSet.instAddCommMonoidUpperSetToLEToPreorderToPartialOrder.proof_1
{α : Type u_1}
[OrderedAddCommGroup α]
(s : UpperSet α)
:
instance
UpperSet.instCommMonoidUpperSetToLEToPreorderToPartialOrder
{α : Type u_1}
[OrderedCommGroup α]
:
CommMonoid (UpperSet α)
instance
LowerSet.instZeroLowerSetToLEToPreorderToPartialOrder
{α : Type u_1}
[OrderedAddCommGroup α]
:
Equations
- LowerSet.instZeroLowerSetToLEToPreorderToPartialOrder = { zero := LowerSet.Iic 0 }
Equations
- LowerSet.instOneLowerSetToLEToPreorderToPartialOrder = { one := LowerSet.Iic 1 }
instance
LowerSet.instAddLowerSetToLEToPreorderToPartialOrder
{α : Type u_1}
[OrderedAddCommGroup α]
:
Equations
- One or more equations did not get rendered due to their size.
theorem
LowerSet.instAddLowerSetToLEToPreorderToPartialOrder.proof_1
{α : Type u_1}
[OrderedAddCommGroup α]
(s : LowerSet α)
(t : LowerSet α)
:
IsLowerSet (s.carrier + ↑t)
Equations
- One or more equations did not get rendered due to their size.
theorem
LowerSet.instSubLowerSetToLEToPreorderToPartialOrder.proof_1
{α : Type u_1}
[OrderedAddCommGroup α]
(s : LowerSet α)
(t : LowerSet α)
:
IsLowerSet (s.carrier - ↑t)
instance
LowerSet.instSubLowerSetToLEToPreorderToPartialOrder
{α : Type u_1}
[OrderedAddCommGroup α]
:
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
instance
LowerSet.instVAddLowerSetToLEToPreorderToPartialOrder
{α : Type u_1}
[OrderedAddCommGroup α]
:
Equations
- One or more equations did not get rendered due to their size.
theorem
LowerSet.instVAddLowerSetToLEToPreorderToPartialOrder.proof_1
{α : Type u_1}
[OrderedAddCommGroup α]
(a : α)
(s : LowerSet α)
:
IsLowerSet (a +ᵥ s.carrier)
instance
LowerSet.instSMulLowerSetToLEToPreorderToPartialOrder
{α : Type u_1}
[OrderedCommGroup α]
:
Equations
- One or more equations did not get rendered due to their size.
@[simp]
@[simp]
@[simp]
@[simp]
instance
LowerSet.instAddActionLowerSetToLEToPreorderToPartialOrderToAddMonoidToSubNegAddMonoidToAddGroupToAddCommGroup
{α : Type u_1}
[OrderedAddCommGroup α]
:
Equations
- One or more equations did not get rendered due to their size.
instance
LowerSet.instMulActionLowerSetToLEToPreorderToPartialOrderToMonoidToDivInvMonoidToGroupToCommGroup
{α : Type u_1}
[OrderedCommGroup α]
:
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
theorem
LowerSet.addCommSemigroup.proof_1
{α : Type u_1}
[OrderedAddCommGroup α]
:
Function.Injective SetLike.coe
theorem
LowerSet.addCommSemigroup.proof_2
{α : Type u_1}
[OrderedAddCommGroup α]
(a : LowerSet α)
(b : LowerSet α)
:
Equations
- One or more equations did not get rendered due to their size.
instance
LowerSet.instAddCommMonoidLowerSetToLEToPreorderToPartialOrder
{α : Type u_1}
[OrderedAddCommGroup α]
:
theorem
LowerSet.instAddCommMonoidLowerSetToLEToPreorderToPartialOrder.proof_1
{α : Type u_1}
[OrderedAddCommGroup α]
(s : LowerSet α)
:
theorem
LowerSet.instAddCommMonoidLowerSetToLEToPreorderToPartialOrder.proof_2
{α : Type u_1}
[OrderedAddCommGroup α]
:
theorem
LowerSet.instAddCommMonoidLowerSetToLEToPreorderToPartialOrder.proof_3
{α : Type u_1}
[OrderedAddCommGroup α]
:
theorem
LowerSet.instAddCommMonoidLowerSetToLEToPreorderToPartialOrder.proof_4
{α : Type u_1}
[OrderedAddCommGroup α]
(a : LowerSet α)
(b : LowerSet α)
:
instance
LowerSet.instCommMonoidLowerSetToLEToPreorderToPartialOrder
{α : Type u_1}
[OrderedCommGroup α]
:
CommMonoid (LowerSet α)
@[simp]
theorem
upperClosure_vadd
{α : Type u_1}
[OrderedAddCommGroup α]
(s : Set α)
(a : α)
:
upperClosure (a +ᵥ s) = a +ᵥ upperClosure s
@[simp]
theorem
upperClosure_smul
{α : Type u_1}
[OrderedCommGroup α]
(s : Set α)
(a : α)
:
upperClosure (a • s) = a • upperClosure s
@[simp]
theorem
lowerClosure_vadd
{α : Type u_1}
[OrderedAddCommGroup α]
(s : Set α)
(a : α)
:
lowerClosure (a +ᵥ s) = a +ᵥ lowerClosure s
@[simp]
theorem
lowerClosure_smul
{α : Type u_1}
[OrderedCommGroup α]
(s : Set α)
(a : α)
:
lowerClosure (a • s) = a • lowerClosure s
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 α)
:
upperClosure (s + t) = upperClosure s + upperClosure t
@[simp]
theorem
upperClosure_mul_distrib
{α : Type u_1}
[OrderedCommGroup α]
(s : Set α)
(t : Set α)
:
upperClosure (s * t) = upperClosure s * upperClosure t
@[simp]
theorem
lowerClosure_add_distrib
{α : Type u_1}
[OrderedAddCommGroup α]
(s : Set α)
(t : Set α)
:
lowerClosure (s + t) = lowerClosure s + lowerClosure t
@[simp]
theorem
lowerClosure_mul_distrib
{α : Type u_1}
[OrderedCommGroup α]
(s : Set α)
(t : Set α)
:
lowerClosure (s * t) = lowerClosure s * lowerClosure t