Small instances for pointwise operations #
instance
small_neg
{α : Type u_1}
(s : Set α)
[InvolutiveNeg α]
[Small.{u, u_1} ↑s]
:
Small.{u, u_1} ↑(-s)
instance
small_add
{α : Type u_1}
(s t : Set α)
[Add α]
[Small.{u, u_1} ↑s]
[Small.{u, u_1} ↑t]
:
Small.{u, u_1} ↑(s + t)
instance
small_sub
{α : Type u_1}
(s t : Set α)
[Sub α]
[Small.{u, u_1} ↑s]
[Small.{u, u_1} ↑t]
:
Small.{u, u_1} ↑(s - t)
instance
small_mul
{α : Type u_1}
(s t : Set α)
[Mul α]
[Small.{u, u_1} ↑s]
[Small.{u, u_1} ↑t]
:
Small.{u, u_1} ↑(s * t)
instance
small_div
{α : Type u_1}
(s t : Set α)
[Div α]
[Small.{u, u_1} ↑s]
[Small.{u, u_1} ↑t]
:
Small.{u, u_1} ↑(s / t)