Algebraic operations on upper/lower sets #

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

theorem IsUpperSet.smul_subset {α : Type u_1} [CommMonoid α] [PartialOrder α] [IsOrderedMonoid α] {s : Set α} {x : α} (hs : IsUpperSet s) (hx : 1 ≤ x) :

x • s ⊆ s

source

theorem IsUpperSet.vadd_subset {α : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] {s : Set α} {x : α} (hs : IsUpperSet s) (hx : 0 ≤ x) :

x +ᵥ s ⊆ s

source

theorem IsLowerSet.smul_subset {α : Type u_1} [CommMonoid α] [PartialOrder α] [IsOrderedMonoid α] {s : Set α} {x : α} (hs : IsLowerSet s) (hx : x ≤ 1) :

x • s ⊆ s

source

theorem IsLowerSet.vadd_subset {α : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] {s : Set α} {x : α} (hs : IsLowerSet s) (hx : x ≤ 0) :

x +ᵥ s ⊆ s

source

theorem IsUpperSet.smul {α : Type u_1} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] {s : Set α} {a : α} (hs : IsUpperSet s) :

IsUpperSet (a • s)

source

theorem IsUpperSet.vadd {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {s : Set α} {a : α} (hs : IsUpperSet s) :

IsUpperSet (a +ᵥ s)

source

theorem IsLowerSet.smul {α : Type u_1} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] {s : Set α} {a : α} (hs : IsLowerSet s) :

IsLowerSet (a • s)

source

theorem IsLowerSet.vadd {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {s : Set α} {a : α} (hs : IsLowerSet s) :

IsLowerSet (a +ᵥ s)

source

theorem Set.OrdConnected.smul {α : Type u_1} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] {s : Set α} {a : α} (hs : s.OrdConnected) :

(a • s).OrdConnected

source

theorem Set.OrdConnected.vadd {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {s : Set α} {a : α} (hs : s.OrdConnected) :

(a +ᵥ s).OrdConnected

source

theorem IsUpperSet.mul_left {α : Type u_1} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] {s t : Set α} (ht : IsUpperSet t) :

IsUpperSet (s * t)

source

theorem IsUpperSet.add_left {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {s t : Set α} (ht : IsUpperSet t) :

IsUpperSet (s + t)

source

theorem IsUpperSet.mul_right {α : Type u_1} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] {s t : Set α} (hs : IsUpperSet s) :

IsUpperSet (s * t)

source

theorem IsUpperSet.add_right {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {s t : Set α} (hs : IsUpperSet s) :

IsUpperSet (s + t)

source

theorem IsLowerSet.mul_left {α : Type u_1} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] {s t : Set α} (ht : IsLowerSet t) :

IsLowerSet (s * t)

source

theorem IsLowerSet.add_left {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {s t : Set α} (ht : IsLowerSet t) :

IsLowerSet (s + t)

source

theorem IsLowerSet.mul_right {α : Type u_1} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] {s t : Set α} (hs : IsLowerSet s) :

IsLowerSet (s * t)

source

theorem IsLowerSet.add_right {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {s t : Set α} (hs : IsLowerSet s) :

IsLowerSet (s + t)

source

theorem IsUpperSet.inv {α : Type u_1} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] {s : Set α} (hs : IsUpperSet s) :

IsLowerSet s⁻¹

source

theorem IsUpperSet.neg {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {s : Set α} (hs : IsUpperSet s) :

IsLowerSet (-s)

source

theorem IsLowerSet.inv {α : Type u_1} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] {s : Set α} (hs : IsLowerSet s) :

IsUpperSet s⁻¹

source

theorem IsLowerSet.neg {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {s : Set α} (hs : IsLowerSet s) :

IsUpperSet (-s)

source

theorem IsUpperSet.div_left {α : Type u_1} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] {s t : Set α} (ht : IsUpperSet t) :

IsLowerSet (s / t)

source

theorem IsUpperSet.sub_left {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {s t : Set α} (ht : IsUpperSet t) :

IsLowerSet (s - t)

source

theorem IsUpperSet.div_right {α : Type u_1} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] {s t : Set α} (hs : IsUpperSet s) :

IsUpperSet (s / t)

source

theorem IsUpperSet.sub_right {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {s t : Set α} (hs : IsUpperSet s) :

IsUpperSet (s - t)

source

theorem IsLowerSet.div_left {α : Type u_1} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] {s t : Set α} (ht : IsLowerSet t) :

IsUpperSet (s / t)

source

theorem IsLowerSet.sub_left {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {s t : Set α} (ht : IsLowerSet t) :

IsUpperSet (s - t)

source

theorem IsLowerSet.div_right {α : Type u_1} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] {s t : Set α} (hs : IsLowerSet s) :

IsLowerSet (s / t)

source

theorem IsLowerSet.sub_right {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {s t : Set α} (hs : IsLowerSet s) :

IsLowerSet (s - t)

source

instance UpperSet.instOne {α : Type u_1} [CommGroup α] [PartialOrder α] :

One (UpperSet α)

Equations

source

instance UpperSet.instZero {α : Type u_1} [AddCommGroup α] [PartialOrder α] :

Zero (UpperSet α)

Equations

source

instance UpperSet.instMul {α : Type u_1} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] :

Mul (UpperSet α)

Equations

source

instance UpperSet.instAdd {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] :

Add (UpperSet α)

Equations

source

instance UpperSet.instDiv {α : Type u_1} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] :

Div (UpperSet α)

Equations

source

instance UpperSet.instSub {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] :

Sub (UpperSet α)

Equations

source

instance UpperSet.instSMul {α : Type u_1} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] :

SMul α (UpperSet α)

Equations

source

instance UpperSet.instVAdd {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] :

VAdd α (UpperSet α)

Equations

source

@[simp]

theorem UpperSet.coe_one {α : Type u_1} [CommGroup α] [PartialOrder α] :

↑1 = Set.Ici 1

source

@[simp]

theorem UpperSet.coe_zero {α : Type u_1} [AddCommGroup α] [PartialOrder α] :

↑0 = Set.Ici 0

source

@[simp]

theorem UpperSet.coe_mul {α : Type u_1} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] (s t : UpperSet α) :

↑(s * t) = ↑s * ↑t

source

@[simp]

theorem UpperSet.coe_add {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] (s t : UpperSet α) :

↑(s + t) = ↑s + ↑t

source

@[simp]

theorem UpperSet.coe_div {α : Type u_1} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] (s t : UpperSet α) :

↑(s / t) = ↑s / ↑t

source

@[simp]

theorem UpperSet.coe_sub {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] (s t : UpperSet α) :

↑(s - t) = ↑s - ↑t

source

@[simp]

theorem UpperSet.Ici_one {α : Type u_1} [CommGroup α] [PartialOrder α] :

Ici 1 = 1

source

@[simp]

theorem UpperSet.Ici_zero {α : Type u_1} [AddCommGroup α] [PartialOrder α] :

Ici 0 = 0

source

instance UpperSet.instMulAction {α : Type u_1} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] :

MulAction α (UpperSet α)

Equations

source

instance UpperSet.instAddAction {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] :

AddAction α (UpperSet α)

Equations

source

instance UpperSet.commSemigroup {α : Type u_1} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] :

CommSemigroup (UpperSet α)

Equations

source

instance UpperSet.addCommSemigroup {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] :

AddCommSemigroup (UpperSet α)

Equations

source

instance UpperSet.instCommMonoid {α : Type u_1} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] :

CommMonoid (UpperSet α)

Equations

source

instance UpperSet.instAddCommMonoid {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] :

AddCommMonoid (UpperSet α)

Equations

source

instance LowerSet.instOne {α : Type u_1} [CommGroup α] [PartialOrder α] :

One (LowerSet α)

Equations

source

instance LowerSet.instZero {α : Type u_1} [AddCommGroup α] [PartialOrder α] :

Zero (LowerSet α)

Equations

source

instance LowerSet.instMul {α : Type u_1} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] :

Mul (LowerSet α)

Equations

source

instance LowerSet.instAdd {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] :

Add (LowerSet α)

Equations

source

instance LowerSet.instDiv {α : Type u_1} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] :

Div (LowerSet α)

Equations

source

instance LowerSet.instSub {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] :

Sub (LowerSet α)

Equations

source

instance LowerSet.instSMul {α : Type u_1} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] :

SMul α (LowerSet α)

Equations

source

instance LowerSet.instVAdd {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] :

VAdd α (LowerSet α)

Equations

source

@[simp]

theorem LowerSet.coe_mul {α : Type u_1} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] (s t : LowerSet α) :

↑(s * t) = ↑s * ↑t

source

@[simp]

theorem LowerSet.coe_add {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] (s t : LowerSet α) :

↑(s + t) = ↑s + ↑t

source

@[simp]

theorem LowerSet.coe_div {α : Type u_1} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] (s t : LowerSet α) :

↑(s / t) = ↑s / ↑t

source

@[simp]

theorem LowerSet.coe_sub {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] (s t : LowerSet α) :

↑(s - t) = ↑s - ↑t

source

@[simp]

theorem LowerSet.Iic_one {α : Type u_1} [CommGroup α] [PartialOrder α] :

Iic 1 = 1

source

@[simp]

theorem LowerSet.Iic_zero {α : Type u_1} [AddCommGroup α] [PartialOrder α] :

Iic 0 = 0

source

instance LowerSet.instMulAction {α : Type u_1} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] :

MulAction α (LowerSet α)

Equations

source

instance LowerSet.instAddAction {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] :

AddAction α (LowerSet α)

Equations

source

instance LowerSet.commSemigroup {α : Type u_1} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] :

CommSemigroup (LowerSet α)

Equations

source

instance LowerSet.addCommSemigroup {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] :

AddCommSemigroup (LowerSet α)

Equations

source

instance LowerSet.instCommMonoid {α : Type u_1} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] :

CommMonoid (LowerSet α)

Equations

source

instance LowerSet.instAddCommMonoid {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] :

AddCommMonoid (LowerSet α)

Equations

source

@[simp]

theorem upperClosure_one {α : Type u_1} [CommGroup α] [PartialOrder α] :

upperClosure 1 = 1

source

@[simp]

theorem upperClosure_zero {α : Type u_1} [AddCommGroup α] [PartialOrder α] :

upperClosure 0 = 0

source

@[simp]

theorem lowerClosure_one {α : Type u_1} [CommGroup α] [PartialOrder α] :

lowerClosure 1 = 1

source

@[simp]

theorem lowerClosure_zero {α : Type u_1} [AddCommGroup α] [PartialOrder α] :

lowerClosure 0 = 0

source

@[simp]

theorem upperClosure_smul {α : Type u_1} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] (s : Set α) (a : α) :

upperClosure (a • s) = a • upperClosure s

source

@[simp]

theorem upperClosure_vadd {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] (s : Set α) (a : α) :

upperClosure (a +ᵥ s) = a +ᵥ upperClosure s

source

@[simp]

theorem lowerClosure_smul {α : Type u_1} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] (s : Set α) (a : α) :

lowerClosure (a • s) = a • lowerClosure s

source

@[simp]

theorem lowerClosure_vadd {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] (s : Set α) (a : α) :

lowerClosure (a +ᵥ s) = a +ᵥ lowerClosure s

source

theorem mul_upperClosure {α : Type u_1} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] (s t : Set α) :

s * ↑(upperClosure t) = ↑(upperClosure (s * t))

source

theorem add_upperClosure {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] (s t : Set α) :

s + ↑(upperClosure t) = ↑(upperClosure (s + t))

source

theorem mul_lowerClosure {α : Type u_1} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] (s t : Set α) :

s * ↑(lowerClosure t) = ↑(lowerClosure (s * t))

source

theorem add_lowerClosure {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] (s t : Set α) :

s + ↑(lowerClosure t) = ↑(lowerClosure (s + t))

source

theorem upperClosure_mul {α : Type u_1} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] (s t : Set α) :

↑(upperClosure s) * t = ↑(upperClosure (s * t))

source

theorem upperClosure_add {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] (s t : Set α) :

↑(upperClosure s) + t = ↑(upperClosure (s + t))

source

theorem lowerClosure_mul {α : Type u_1} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] (s t : Set α) :

↑(lowerClosure s) * t = ↑(lowerClosure (s * t))

source

theorem lowerClosure_add {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] (s t : Set α) :

↑(lowerClosure s) + t = ↑(lowerClosure (s + t))

source

@[simp]

theorem upperClosure_mul_distrib {α : Type u_1} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] (s t : Set α) :

upperClosure (s * t) = upperClosure s * upperClosure t

source

@[simp]

theorem upperClosure_add_distrib {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] (s t : Set α) :

upperClosure (s + t) = upperClosure s + upperClosure t

source

@[simp]

theorem lowerClosure_mul_distrib {α : Type u_1} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] (s t : Set α) :

lowerClosure (s * t) = lowerClosure s * lowerClosure t

source

@[simp]

theorem lowerClosure_add_distrib {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] (s t : Set α) :

lowerClosure (s + t) = lowerClosure s + lowerClosure t

Documentation

Mathlib.Algebra.Order.UpperLower

Algebraic operations on upper/lower sets #