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

source

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

x • s ⊆ s

source

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

x +ᵥ s ⊆ s

source

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

x • s ⊆ s

source

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

IsUpperSet (a +ᵥ s)

source

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

IsUpperSet (a • s)

source

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

IsLowerSet (a +ᵥ s)

source

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

IsLowerSet (a • s)

source

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

Set.OrdConnected (a +ᵥ s)

source

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

Set.OrdConnected (a • s)

source

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

IsUpperSet (s + t)

source

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

IsUpperSet (s * t)

source

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

IsUpperSet (s + t)

source

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

IsUpperSet (s * t)

source

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

IsLowerSet (s + t)

source

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

IsLowerSet (s * t)

source

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

IsLowerSet (s + t)

source

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

IsLowerSet (s * t)

source

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

IsLowerSet (-s)

source

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

IsLowerSet s⁻¹

source

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

IsUpperSet (-s)

source

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

IsUpperSet s⁻¹

source

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

IsLowerSet (s - t)

source

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

IsLowerSet (s / t)

source

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

IsUpperSet (s - t)

source

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

IsUpperSet (s / t)

source

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

IsUpperSet (s - t)

source

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

IsUpperSet (s / t)

source

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

IsLowerSet (s - t)

source

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

IsLowerSet (s / t)

source

instance UpperSet.instZeroUpperSetToLEToPreorderToPartialOrder {α : Type u_1} [OrderedAddCommGroup α] :

Zero (UpperSet α)

Equations

UpperSet.instZeroUpperSetToLEToPreorderToPartialOrder = { zero := UpperSet.Ici 0 }

source

instance UpperSet.instOneUpperSetToLEToPreorderToPartialOrder {α : Type u_1} [OrderedCommGroup α] :

One (UpperSet α)

Equations

UpperSet.instOneUpperSetToLEToPreorderToPartialOrder = { one := UpperSet.Ici 1 }

source

instance UpperSet.instAddUpperSetToLEToPreorderToPartialOrder {α : Type u_1} [OrderedAddCommGroup α] :

Add (UpperSet α)

Equations

UpperSet.instAddUpperSetToLEToPreorderToPartialOrder = { add := fun (s t : UpperSet α) => { carrier := Set.image2 (fun (x x_1 : α) => x + x_1) ↑s ↑t, upper' := ⋯ } }

source

theorem UpperSet.instAddUpperSetToLEToPreorderToPartialOrder.proof_1 {α : Type u_1} [OrderedAddCommGroup α] (s : UpperSet α) (t : UpperSet α) :

IsUpperSet (s.carrier + ↑t)

source

instance UpperSet.instMulUpperSetToLEToPreorderToPartialOrder {α : Type u_1} [OrderedCommGroup α] :

Mul (UpperSet α)

Equations

UpperSet.instMulUpperSetToLEToPreorderToPartialOrder = { mul := fun (s t : UpperSet α) => { carrier := Set.image2 (fun (x x_1 : α) => x * x_1) ↑s ↑t, upper' := ⋯ } }

source

theorem UpperSet.instSubUpperSetToLEToPreorderToPartialOrder.proof_1 {α : Type u_1} [OrderedAddCommGroup α] (s : UpperSet α) (t : UpperSet α) :

IsUpperSet (s.carrier - ↑t)

source

instance UpperSet.instSubUpperSetToLEToPreorderToPartialOrder {α : Type u_1} [OrderedAddCommGroup α] :

Sub (UpperSet α)

Equations

UpperSet.instSubUpperSetToLEToPreorderToPartialOrder = { sub := fun (s t : UpperSet α) => { carrier := Set.image2 (fun (x x_1 : α) => x - x_1) ↑s ↑t, upper' := ⋯ } }

source

instance UpperSet.instDivUpperSetToLEToPreorderToPartialOrder {α : Type u_1} [OrderedCommGroup α] :

Div (UpperSet α)

Equations

UpperSet.instDivUpperSetToLEToPreorderToPartialOrder = { div := fun (s t : UpperSet α) => { carrier := Set.image2 (fun (x x_1 : α) => x / x_1) ↑s ↑t, upper' := ⋯ } }

source

instance UpperSet.instVAddUpperSetToLEToPreorderToPartialOrder {α : Type u_1} [OrderedAddCommGroup α] :

VAdd α (UpperSet α)

Equations

UpperSet.instVAddUpperSetToLEToPreorderToPartialOrder = { vadd := fun (a : α) (s : UpperSet α) => { carrier := (fun (x : α) => a +ᵥ x) '' ↑s, upper' := ⋯ } }

source

theorem UpperSet.instVAddUpperSetToLEToPreorderToPartialOrder.proof_1 {α : Type u_1} [OrderedAddCommGroup α] (a : α) (s : UpperSet α) :

IsUpperSet (a +ᵥ s.carrier)

source

instance UpperSet.instSMulUpperSetToLEToPreorderToPartialOrder {α : Type u_1} [OrderedCommGroup α] :

SMul α (UpperSet α)

Equations

UpperSet.instSMulUpperSetToLEToPreorderToPartialOrder = { smul := fun (a : α) (s : UpperSet α) => { carrier := (fun (x : α) => a • x) '' ↑s, upper' := ⋯ } }

source

@[simp]

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

↑0 = Set.Ici 0

source

@[simp]

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

↑1 = Set.Ici 1

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

UpperSet.Ici 0 = 0

source

@[simp]

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

UpperSet.Ici 1 = 1

source

theorem UpperSet.instAddActionUpperSetToLEToPreorderToPartialOrderToAddMonoidToSubNegAddMonoidToAddGroupToAddCommGroup.proof_1 {α : Type u_1} [OrderedAddCommGroup α] :

Function.Injective SetLike.coe

source

theorem UpperSet.instAddActionUpperSetToLEToPreorderToPartialOrderToAddMonoidToSubNegAddMonoidToAddGroupToAddCommGroup.proof_2 {α : Type u_1} [OrderedAddCommGroup α] :

∀ (x : α) (x_1 : UpperSet α), ↑(x +ᵥ x_1) = ↑(x +ᵥ x_1)

source

instance UpperSet.instAddActionUpperSetToLEToPreorderToPartialOrderToAddMonoidToSubNegAddMonoidToAddGroupToAddCommGroup {α : Type u_1} [OrderedAddCommGroup α] :

AddAction α (UpperSet α)

Equations

UpperSet.instAddActionUpperSetToLEToPreorderToPartialOrderToAddMonoidToSubNegAddMonoidToAddGroupToAddCommGroup = Function.Injective.addAction SetLike.coe ⋯ ⋯

source

instance UpperSet.instMulActionUpperSetToLEToPreorderToPartialOrderToMonoidToDivInvMonoidToGroupToCommGroup {α : Type u_1} [OrderedCommGroup α] :

MulAction α (UpperSet α)

Equations

UpperSet.instMulActionUpperSetToLEToPreorderToPartialOrderToMonoidToDivInvMonoidToGroupToCommGroup = Function.Injective.mulAction SetLike.coe ⋯ ⋯

source

theorem UpperSet.addCommSemigroup.proof_1 {α : Type u_1} [OrderedAddCommGroup α] :

Function.Injective SetLike.coe

source

instance UpperSet.addCommSemigroup {α : Type u_1} [OrderedAddCommGroup α] :

AddCommSemigroup (UpperSet α)

Equations

UpperSet.addCommSemigroup = let __src := Function.Injective.addCommSemigroup SetLike.coe ⋯ ⋯; AddCommSemigroup.mk ⋯

source

theorem UpperSet.addCommSemigroup.proof_2 {α : Type u_1} [OrderedAddCommGroup α] (a : UpperSet α) (b : UpperSet α) :

a + b = b + a

source

instance UpperSet.commSemigroup {α : Type u_1} [OrderedCommGroup α] :

CommSemigroup (UpperSet α)

Equations

UpperSet.commSemigroup = let __src := Function.Injective.commSemigroup SetLike.coe ⋯ ⋯; CommSemigroup.mk ⋯

source

theorem UpperSet.instAddCommMonoidUpperSetToLEToPreorderToPartialOrder.proof_4 {α : Type u_1} [OrderedAddCommGroup α] (a : UpperSet α) (b : UpperSet α) :

a + b = b + a

source

theorem UpperSet.instAddCommMonoidUpperSetToLEToPreorderToPartialOrder.proof_2 {α : Type u_1} [OrderedAddCommGroup α] :

∀ (x : UpperSet α), nsmulRec 0 x = nsmulRec 0 x

source

theorem UpperSet.instAddCommMonoidUpperSetToLEToPreorderToPartialOrder.proof_3 {α : Type u_1} [OrderedAddCommGroup α] :

∀ (n : ℕ) (x : UpperSet α), nsmulRec (n + 1) x = nsmulRec (n + 1) x

source

instance UpperSet.instAddCommMonoidUpperSetToLEToPreorderToPartialOrder {α : Type u_1} [OrderedAddCommGroup α] :

AddCommMonoid (UpperSet α)

Equations

UpperSet.instAddCommMonoidUpperSetToLEToPreorderToPartialOrder = let __src := UpperSet.addCommSemigroup; AddCommMonoid.mk ⋯

source

theorem UpperSet.instAddCommMonoidUpperSetToLEToPreorderToPartialOrder.proof_1 {α : Type u_1} [OrderedAddCommGroup α] (s : UpperSet α) :

s + 0 = s

source

instance UpperSet.instCommMonoidUpperSetToLEToPreorderToPartialOrder {α : Type u_1} [OrderedCommGroup α] :

CommMonoid (UpperSet α)

Equations

UpperSet.instCommMonoidUpperSetToLEToPreorderToPartialOrder = let __src := UpperSet.commSemigroup; CommMonoid.mk ⋯

source

instance LowerSet.instZeroLowerSetToLEToPreorderToPartialOrder {α : Type u_1} [OrderedAddCommGroup α] :

Zero (LowerSet α)

Equations

LowerSet.instZeroLowerSetToLEToPreorderToPartialOrder = { zero := LowerSet.Iic 0 }

source

instance LowerSet.instOneLowerSetToLEToPreorderToPartialOrder {α : Type u_1} [OrderedCommGroup α] :

One (LowerSet α)

Equations

LowerSet.instOneLowerSetToLEToPreorderToPartialOrder = { one := LowerSet.Iic 1 }

source

instance LowerSet.instAddLowerSetToLEToPreorderToPartialOrder {α : Type u_1} [OrderedAddCommGroup α] :

Add (LowerSet α)

Equations

LowerSet.instAddLowerSetToLEToPreorderToPartialOrder = { add := fun (s t : LowerSet α) => { carrier := Set.image2 (fun (x x_1 : α) => x + x_1) ↑s ↑t, lower' := ⋯ } }

source

theorem LowerSet.instAddLowerSetToLEToPreorderToPartialOrder.proof_1 {α : Type u_1} [OrderedAddCommGroup α] (s : LowerSet α) (t : LowerSet α) :

IsLowerSet (s.carrier + ↑t)

source

instance LowerSet.instMulLowerSetToLEToPreorderToPartialOrder {α : Type u_1} [OrderedCommGroup α] :

Mul (LowerSet α)

Equations

LowerSet.instMulLowerSetToLEToPreorderToPartialOrder = { mul := fun (s t : LowerSet α) => { carrier := Set.image2 (fun (x x_1 : α) => x * x_1) ↑s ↑t, lower' := ⋯ } }

source

theorem LowerSet.instSubLowerSetToLEToPreorderToPartialOrder.proof_1 {α : Type u_1} [OrderedAddCommGroup α] (s : LowerSet α) (t : LowerSet α) :

IsLowerSet (s.carrier - ↑t)

source

instance LowerSet.instSubLowerSetToLEToPreorderToPartialOrder {α : Type u_1} [OrderedAddCommGroup α] :

Sub (LowerSet α)

Equations

LowerSet.instSubLowerSetToLEToPreorderToPartialOrder = { sub := fun (s t : LowerSet α) => { carrier := Set.image2 (fun (x x_1 : α) => x - x_1) ↑s ↑t, lower' := ⋯ } }

source

instance LowerSet.instDivLowerSetToLEToPreorderToPartialOrder {α : Type u_1} [OrderedCommGroup α] :

Div (LowerSet α)

Equations

LowerSet.instDivLowerSetToLEToPreorderToPartialOrder = { div := fun (s t : LowerSet α) => { carrier := Set.image2 (fun (x x_1 : α) => x / x_1) ↑s ↑t, lower' := ⋯ } }

source

instance LowerSet.instVAddLowerSetToLEToPreorderToPartialOrder {α : Type u_1} [OrderedAddCommGroup α] :

VAdd α (LowerSet α)

Equations

LowerSet.instVAddLowerSetToLEToPreorderToPartialOrder = { vadd := fun (a : α) (s : LowerSet α) => { carrier := (fun (x : α) => a +ᵥ x) '' ↑s, lower' := ⋯ } }

source

theorem LowerSet.instVAddLowerSetToLEToPreorderToPartialOrder.proof_1 {α : Type u_1} [OrderedAddCommGroup α] (a : α) (s : LowerSet α) :

IsLowerSet (a +ᵥ s.carrier)

source

instance LowerSet.instSMulLowerSetToLEToPreorderToPartialOrder {α : Type u_1} [OrderedCommGroup α] :

SMul α (LowerSet α)

Equations

LowerSet.instSMulLowerSetToLEToPreorderToPartialOrder = { smul := fun (a : α) (s : LowerSet α) => { carrier := (fun (x : α) => a • x) '' ↑s, lower' := ⋯ } }

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

LowerSet.Iic 0 = 0

source

@[simp]

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

LowerSet.Iic 1 = 1

source

theorem LowerSet.instAddActionLowerSetToLEToPreorderToPartialOrderToAddMonoidToSubNegAddMonoidToAddGroupToAddCommGroup.proof_1 {α : Type u_1} [OrderedAddCommGroup α] :

Function.Injective SetLike.coe

source

theorem LowerSet.instAddActionLowerSetToLEToPreorderToPartialOrderToAddMonoidToSubNegAddMonoidToAddGroupToAddCommGroup.proof_2 {α : Type u_1} [OrderedAddCommGroup α] :

∀ (x : α) (x_1 : LowerSet α), ↑(x +ᵥ x_1) = ↑(x +ᵥ x_1)

source

instance LowerSet.instAddActionLowerSetToLEToPreorderToPartialOrderToAddMonoidToSubNegAddMonoidToAddGroupToAddCommGroup {α : Type u_1} [OrderedAddCommGroup α] :

AddAction α (LowerSet α)

Equations

LowerSet.instAddActionLowerSetToLEToPreorderToPartialOrderToAddMonoidToSubNegAddMonoidToAddGroupToAddCommGroup = Function.Injective.addAction SetLike.coe ⋯ ⋯

source

instance LowerSet.instMulActionLowerSetToLEToPreorderToPartialOrderToMonoidToDivInvMonoidToGroupToCommGroup {α : Type u_1} [OrderedCommGroup α] :

MulAction α (LowerSet α)

Equations

LowerSet.instMulActionLowerSetToLEToPreorderToPartialOrderToMonoidToDivInvMonoidToGroupToCommGroup = Function.Injective.mulAction SetLike.coe ⋯ ⋯

source

instance LowerSet.addCommSemigroup {α : Type u_1} [OrderedAddCommGroup α] :

AddCommSemigroup (LowerSet α)

Equations

LowerSet.addCommSemigroup = let __src := Function.Injective.addCommSemigroup SetLike.coe ⋯ ⋯; AddCommSemigroup.mk ⋯

source

theorem LowerSet.addCommSemigroup.proof_1 {α : Type u_1} [OrderedAddCommGroup α] :

Function.Injective SetLike.coe

source

theorem LowerSet.addCommSemigroup.proof_2 {α : Type u_1} [OrderedAddCommGroup α] (a : LowerSet α) (b : LowerSet α) :

a + b = b + a

source

instance LowerSet.commSemigroup {α : Type u_1} [OrderedCommGroup α] :

CommSemigroup (LowerSet α)

Equations

LowerSet.commSemigroup = let __src := Function.Injective.commSemigroup SetLike.coe ⋯ ⋯; CommSemigroup.mk ⋯

source

instance LowerSet.instAddCommMonoidLowerSetToLEToPreorderToPartialOrder {α : Type u_1} [OrderedAddCommGroup α] :

AddCommMonoid (LowerSet α)

Equations

LowerSet.instAddCommMonoidLowerSetToLEToPreorderToPartialOrder = let __src := LowerSet.addCommSemigroup; AddCommMonoid.mk ⋯

source

theorem LowerSet.instAddCommMonoidLowerSetToLEToPreorderToPartialOrder.proof_1 {α : Type u_1} [OrderedAddCommGroup α] (s : LowerSet α) :

s + 0 = s

source

theorem LowerSet.instAddCommMonoidLowerSetToLEToPreorderToPartialOrder.proof_2 {α : Type u_1} [OrderedAddCommGroup α] :

∀ (x : LowerSet α), nsmulRec 0 x = nsmulRec 0 x

source

theorem LowerSet.instAddCommMonoidLowerSetToLEToPreorderToPartialOrder.proof_3 {α : Type u_1} [OrderedAddCommGroup α] :

∀ (n : ℕ) (x : LowerSet α), nsmulRec (n + 1) x = nsmulRec (n + 1) x

source

theorem LowerSet.instAddCommMonoidLowerSetToLEToPreorderToPartialOrder.proof_4 {α : Type u_1} [OrderedAddCommGroup α] (a : LowerSet α) (b : LowerSet α) :

a + b = b + a

source

instance LowerSet.instCommMonoidLowerSetToLEToPreorderToPartialOrder {α : Type u_1} [OrderedCommGroup α] :

CommMonoid (LowerSet α)

Equations

LowerSet.instCommMonoidLowerSetToLEToPreorderToPartialOrder = let __src := LowerSet.commSemigroup; CommMonoid.mk ⋯

source

@[simp]

theorem upperClosure_zero {α : Type u_1} [OrderedAddCommGroup α] :

upperClosure 0 = 0

source

@[simp]

theorem upperClosure_one {α : Type u_1} [OrderedCommGroup α] :

upperClosure 1 = 1

source

@[simp]

theorem lowerClosure_zero {α : Type u_1} [OrderedAddCommGroup α] :

lowerClosure 0 = 0

source

@[simp]

theorem lowerClosure_one {α : Type u_1} [OrderedCommGroup α] :

lowerClosure 1 = 1

source

@[simp]

theorem upperClosure_vadd {α : Type u_1} [OrderedAddCommGroup α] (s : Set α) (a : α) :

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

source

@[simp]

theorem upperClosure_smul {α : Type u_1} [OrderedCommGroup α] (s : Set α) (a : α) :

upperClosure (a • s) = a • upperClosure s

source

@[simp]

theorem lowerClosure_vadd {α : Type u_1} [OrderedAddCommGroup α] (s : Set α) (a : α) :

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

source

@[simp]

theorem lowerClosure_smul {α : Type u_1} [OrderedCommGroup α] (s : Set α) (a : α) :

lowerClosure (a • s) = a • lowerClosure s

source

theorem add_upperClosure {α : Type u_1} [OrderedAddCommGroup α] (s : Set α) (t : Set α) :

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

source

theorem mul_upperClosure {α : Type u_1} [OrderedCommGroup α] (s : Set α) (t : Set α) :

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

source

theorem add_lowerClosure {α : Type u_1} [OrderedAddCommGroup α] (s : Set α) (t : Set α) :

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

source

theorem mul_lowerClosure {α : Type u_1} [OrderedCommGroup α] (s : Set α) (t : Set α) :

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

source

theorem upperClosure_add {α : Type u_1} [OrderedAddCommGroup α] (s : Set α) (t : Set α) :

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

source

theorem upperClosure_mul {α : Type u_1} [OrderedCommGroup α] (s : Set α) (t : Set α) :

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

source

theorem lowerClosure_add {α : Type u_1} [OrderedAddCommGroup α] (s : Set α) (t : Set α) :

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

source

theorem lowerClosure_mul {α : Type u_1} [OrderedCommGroup α] (s : Set α) (t : Set α) :

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

source

@[simp]

theorem upperClosure_add_distrib {α : Type u_1} [OrderedAddCommGroup α] (s : Set α) (t : Set α) :

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

source

@[simp]

theorem upperClosure_mul_distrib {α : Type u_1} [OrderedCommGroup α] (s : Set α) (t : Set α) :

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

source

@[simp]

theorem lowerClosure_add_distrib {α : Type u_1} [OrderedAddCommGroup α] (s : Set α) (t : Set α) :

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

source

@[simp]

theorem lowerClosure_mul_distrib {α : Type u_1} [OrderedCommGroup α] (s : Set α) (t : Set α) :

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

Documentation

Mathlib.Algebra.Order.UpperLower

Algebraic operations on upper/lower sets #