# Subset Check

The function `⊆`

checks whether a set is a subset of another set. It can optionally produce a witness if the subset relation does not hold. The operator can be used in infix notation (`X ⊆ Y`

).

`issubset`

can be used as an alternative name to `⊆`

.

## Examples

We use the following four sets for illustration.

```
using LazySets, LazySets.Approximations, Plots
B1 = Ball1(-ones(2), 1.)
B2 = Ball2(ones(2), 1.)
BI = BallInf(zeros(2), 1.)
H = Hyperrectangle(ones(2), ones(2))
sets = [B1, B2, BI, H]
function plot_sets(sets)
for S in sets
println(S)
plot!(S, 1e-2, fillalpha=0.1)
end
end
function plot_points(points, prefix)
for i in eachindex(points)
p = points[i]
num_occur = length(findfirst(x -> x == p, points[1:i]))
x = p[1]
y = p[2]
if num_occur == 1
x += 0.15
elseif num_occur == 2
y += 0.15
elseif num_occur == 3
x -= 0.15
else
y -= 0.15
end
plot!(Singleton(p))
plot!(annotations=(x, y, text("$(prefix)$(i)")))
end
end
plot1 = plot()
plot_sets(sets)
plot1
```

```
println(B1 ⊆ B2)
w1 = ⊆(B1, B2, true)[2]
println(B1 ⊆ BI)
w2 = ⊆(B1, BI, true)[2]
println(B1 ⊆ H)
w3 = ⊆(B1, H, true)[2]
# 'B2 ⊆ B1' is not supported yet
# w11 = ⊆(B2, B1, true)[2]
println(B2 ⊆ BI)
w4 = ⊆(B2, BI, true)[2]
println(B2 ⊆ H)
println(BI ⊆ B1)
w5 = ⊆(BI, B1, true)[2]
println(BI ⊆ B2)
w6 = ⊆(BI, B2, true)[2]
println(BI ⊆ H)
w7 = ⊆(BI, H, true)[2]
println(H ⊆ B1)
w8 = ⊆(H, B1, true)[2]
println(H ⊆ B2)
w9 = ⊆(H, B2, true)[2]
println(H ⊆ BI)
w10 = ⊆(H, BI, true)[2];
```

```
2-element Vector{Float64}:
2.0
1.0
```

```
witnesses = [w1, w2, w3, w4, w5, w6, w7, w8, w9, w10]
plot1 = plot()
plot_sets(sets)
plot_points(witnesses, "w")
plot1
```

## Methods

`Base.issubset`

— Function`issubset(X::LazySet, Y::LazySet, [witness]::Bool=false, args...)`

Alias for `⊆`

(inclusion check).

**Input**

`X`

– set`Y`

– set`witness`

– (optional, default:`false`

) compute a witness if activated

**Output**

- If
`witness`

option is deactivated:`true`

iff $X ⊆ Y$ - If
`witness`

option is activated:`(true, [])`

iff $X ⊆ Y$`(false, v)`

iff $X ⊈ Y$ and $v ∈ X \setminus Y$

**Notes**

For more documentation see `⊆`

.

`Base.:⊆`

— Function`⊆(X::LazySet, P::LazySet, [witness]::Bool=false)`

Check whether a set is contained in a polyhedral set, and if not, optionally compute a witness.

**Input**

`X`

– inner set`Y`

– outer polyhedral set`witness`

– (optional, default:`false`

) compute a witness if activated

**Output**

- If
`witness`

option is deactivated:`true`

iff $X ⊆ P$ - If
`witness`

option is activated:`(true, [])`

iff $X ⊆ P$`(false, v)`

iff $X ⊈ P$ and $v ∈ X \setminus P$

**Notes**

We require that `constraints_list(P)`

is available.

**Algorithm**

We check inclusion of `X`

in every constraint of `P`

.

`Base.:⊆`

— Function`⊆(S::LazySet, H::AbstractHyperrectangle, [witness]::Bool=false)`

Check whether a set is contained in a hyperrectangular set, and if not, optionally compute a witness.

**Input**

`S`

– inner set`H`

– outer hyperrectangular set`witness`

– (optional, default:`false`

) compute a witness if activated

**Output**

- If
`witness`

option is deactivated:`true`

iff $S ⊆ H$ - If
`witness`

option is activated:`(true, [])`

iff $S ⊆ H$`(false, v)`

iff $S ⊈ H$ and $v ∈ S \setminus H$

**Algorithm**

$S ⊆ H$ iff $\operatorname{ihull}(S) ⊆ H$, where $\operatorname{ihull}$ is the interval-hull operator.

`Base.:⊆`

— Function```
⊆(P::AbstractPolytope, S::LazySet, [witness]::Bool=false;
[algorithm]="constraints")
```

Check whether a polytopic set is contained in a convex set, and if not, optionally compute a witness.

**Input**

`P`

– inner polytopic set`S`

– outer convex set`witness`

– (optional, default:`false`

) compute a witness if activated`algorithm`

– (optional, default:`"constraints"`

) algorithm for the inclusion check; available options are:`"constraints"`

, using the list of constraints of`S`

(requires that`S`

is polyhedral) and support-function evaluations of`S`

`"vertices"`

, using the list of vertices of`P`

and membership evaluations of`S`

**Output**

- If
`witness`

option is deactivated:`true`

iff $P ⊆ S$ - If
`witness`

option is activated:`(true, [])`

iff $P ⊆ S$`(false, v)`

iff $P ⊈ S$ and $v ∈ P \setminus S$

**Algorithm**

`"vertices"`

:

Since $S$ is convex, $P ⊆ S$ iff $v ∈ S$ for all vertices $v$ of $P$.

`Base.:⊆`

— Function`⊆(X::LazySet, P::LazySet, [witness]::Bool=false)`

Check whether a set is contained in a polyhedral set, and if not, optionally compute a witness.

**Input**

`X`

– inner set`Y`

– outer polyhedral set`witness`

– (optional, default:`false`

) compute a witness if activated

**Output**

- If
`witness`

option is deactivated:`true`

iff $X ⊆ P$ - If
`witness`

option is activated:`(true, [])`

iff $X ⊆ P$`(false, v)`

iff $X ⊈ P$ and $v ∈ X \setminus P$

**Notes**

We require that `constraints_list(P)`

is available.

**Algorithm**

We check inclusion of `X`

in every constraint of `P`

.

`⊆(S::LazySet, H::AbstractHyperrectangle, [witness]::Bool=false)`

Check whether a set is contained in a hyperrectangular set, and if not, optionally compute a witness.

**Input**

`S`

– inner set`H`

– outer hyperrectangular set`witness`

– (optional, default:`false`

) compute a witness if activated

**Output**

- If
`witness`

option is deactivated:`true`

iff $S ⊆ H$ - If
`witness`

option is activated:`(true, [])`

iff $S ⊆ H$`(false, v)`

iff $S ⊈ H$ and $v ∈ S \setminus H$

**Algorithm**

$S ⊆ H$ iff $\operatorname{ihull}(S) ⊆ H$, where $\operatorname{ihull}$ is the interval-hull operator.

```
⊆(P::AbstractPolytope, S::LazySet, [witness]::Bool=false;
[algorithm]="constraints")
```

Check whether a polytopic set is contained in a convex set, and if not, optionally compute a witness.

**Input**

`P`

– inner polytopic set`S`

– outer convex set`witness`

– (optional, default:`false`

) compute a witness if activated`algorithm`

– (optional, default:`"constraints"`

) algorithm for the inclusion check; available options are:`"constraints"`

, using the list of constraints of`S`

(requires that`S`

is polyhedral) and support-function evaluations of`S`

`"vertices"`

, using the list of vertices of`P`

and membership evaluations of`S`

**Output**

- If
`witness`

option is deactivated:`true`

iff $P ⊆ S$ - If
`witness`

option is activated:`(true, [])`

iff $P ⊆ S$`(false, v)`

iff $P ⊈ S$ and $v ∈ P \setminus S$

**Algorithm**

`"vertices"`

:

Since $S$ is convex, $P ⊆ S$ iff $v ∈ S$ for all vertices $v$ of $P$.

`⊆(X::LazySet, P::AbstractPolyhedron, [witness]::Bool=false)`

Check whether a convex set is contained in a polyhedral set, and if not, optionally compute a witness.

**Input**

`X`

– inner convex set`P`

– outer polyhedral set`witness`

– (optional, default:`false`

) compute a witness if activated

**Output**

- If
`witness`

option is deactivated:`true`

iff $X ⊆ P$ - If
`witness`

option is activated:`(true, [])`

iff $X ⊆ P$`(false, v)`

iff $X ⊈ P$ and $v ∈ P \setminus X$

**Algorithm**

Since $X$ is convex, we can compare the support function of $X$ and $P$ in each direction of the constraints of $P$.

For witness generation, we use a support vector in the first direction where the above check fails.

`Base.:⊆`

— Method`⊆(X::LazySet, P::LazySet, [witness]::Bool=false)`

Check whether a set is contained in a polyhedral set, and if not, optionally compute a witness.

**Input**

`X`

– inner set`Y`

– outer polyhedral set`witness`

– (optional, default:`false`

) compute a witness if activated

**Output**

- If
`witness`

option is deactivated:`true`

iff $X ⊆ P$ - If
`witness`

option is activated:`(true, [])`

iff $X ⊆ P$`(false, v)`

iff $X ⊈ P$ and $v ∈ X \setminus P$

**Notes**

We require that `constraints_list(P)`

is available.

**Algorithm**

We check inclusion of `X`

in every constraint of `P`

.

`⊆(S::LazySet, H::AbstractHyperrectangle, [witness]::Bool=false)`

Check whether a set is contained in a hyperrectangular set, and if not, optionally compute a witness.

**Input**

`S`

– inner set`H`

– outer hyperrectangular set`witness`

– (optional, default:`false`

) compute a witness if activated

**Output**

- If
`witness`

option is deactivated:`true`

iff $S ⊆ H$ - If
`witness`

option is activated:`(true, [])`

iff $S ⊆ H$`(false, v)`

iff $S ⊈ H$ and $v ∈ S \setminus H$

**Algorithm**

$S ⊆ H$ iff $\operatorname{ihull}(S) ⊆ H$, where $\operatorname{ihull}$ is the interval-hull operator.

```
⊆(P::AbstractPolytope, S::LazySet, [witness]::Bool=false;
[algorithm]="constraints")
```

Check whether a polytopic set is contained in a convex set, and if not, optionally compute a witness.

**Input**

`P`

– inner polytopic set`S`

– outer convex set`witness`

– (optional, default:`false`

) compute a witness if activated`algorithm`

– (optional, default:`"constraints"`

) algorithm for the inclusion check; available options are:`"constraints"`

, using the list of constraints of`S`

(requires that`S`

is polyhedral) and support-function evaluations of`S`

`"vertices"`

, using the list of vertices of`P`

and membership evaluations of`S`

**Output**

- If
`witness`

option is deactivated:`true`

iff $P ⊆ S$ - If
`witness`

option is activated:`(true, [])`

iff $P ⊆ S$`(false, v)`

iff $P ⊈ S$ and $v ∈ P \setminus S$

**Algorithm**

`"vertices"`

:

Since $S$ is convex, $P ⊆ S$ iff $v ∈ S$ for all vertices $v$ of $P$.

`⊆(X::LazySet, P::AbstractPolyhedron, [witness]::Bool=false)`

Check whether a convex set is contained in a polyhedral set, and if not, optionally compute a witness.

**Input**

`X`

– inner convex set`P`

– outer polyhedral set`witness`

– (optional, default:`false`

) compute a witness if activated

**Output**

- If
`witness`

option is deactivated:`true`

iff $X ⊆ P$ - If
`witness`

option is activated:`(true, [])`

iff $X ⊆ P$`(false, v)`

iff $X ⊈ P$ and $v ∈ P \setminus X$

**Algorithm**

Since $X$ is convex, we can compare the support function of $X$ and $P$ in each direction of the constraints of $P$.

For witness generation, we use a support vector in the first direction where the above check fails.

`⊆(Z::AbstractZonotope, H::AbstractHyperrectangle, [witness]::Bool=false)`

Check whether a zonotopic set is contained in a hyperrectangular set.

**Input**

`Z`

– inner zonotopic set`H`

– outer hyperrectangular set`witness`

– (optional, default:`false`

) compute a witness if activated (currently not supported)

**Output**

`true`

iff $Z ⊆ H$.

**Algorithm**

The algorithm is based on Lemma 3.1 in [1].

[1] Mitchell, I. M., Budzis, J., & Bolyachevets, A. *Invariant, viability and discriminating kernel under-approximation via zonotope scaling*. HSCC 2019.

`Base.:⊆`

— Function```
⊆(H1::AbstractHyperrectangle, H2::AbstractHyperrectangle,
[witness]::Bool=false)
```

Check whether a given hyperrectangular set is contained in another hyperrectangular set, and if not, optionally compute a witness.

**Input**

`H1`

– inner hyperrectangular set`H2`

– outer hyperrectangular set`witness`

– (optional, default:`false`

) compute a witness if activated

**Output**

- If
`witness`

option is deactivated:`true`

iff $H1 ⊆ H2$ - If
`witness`

option is activated:`(true, [])`

iff $H1 ⊆ H2$`(false, v)`

iff $H1 ⊈ H2$ and $v ∈ H1 \setminus H2$

**Algorithm**

$H1 ⊆ H2$ iff $c_1 + r_1 ≤ c_2 + r_2 ∧ c_1 - r_1 ≥ c_2 - r_2$ iff $r_1 - r_2 ≤ c_1 - c_2 ≤ -(r_1 - r_2)$, where $≤$ is taken component-wise.

`Base.:⊆`

— Function`⊆(X::LazySet, P::AbstractPolyhedron, [witness]::Bool=false)`

Check whether a convex set is contained in a polyhedral set, and if not, optionally compute a witness.

**Input**

`X`

– inner convex set`P`

– outer polyhedral set`witness`

– (optional, default:`false`

) compute a witness if activated

**Output**

- If
`witness`

option is deactivated:`true`

iff $X ⊆ P$ - If
`witness`

option is activated:`(true, [])`

iff $X ⊆ P$`(false, v)`

iff $X ⊈ P$ and $v ∈ P \setminus X$

**Algorithm**

Since $X$ is convex, we can compare the support function of $X$ and $P$ in each direction of the constraints of $P$.

For witness generation, we use a support vector in the first direction where the above check fails.

`Base.:⊆`

— Function`⊆(S::AbstractSingleton, X::LazySet, [witness]::Bool=false)`

Check whether a given set with a single value is contained in another set, and if not, optionally compute a witness.

**Input**

`S`

– inner set with a single value`X`

– outer set`witness`

– (optional, default:`false`

) compute a witness if activated

**Output**

- If
`witness`

option is deactivated:`true`

iff $S ⊆ X$ - If
`witness`

option is activated:`(true, [])`

iff $S ⊆ X$`(false, v)`

iff $S ⊈ X$ and $v ∈ S \setminus X$

`Base.:⊆`

— Function`⊆(X::LazySet, P::LazySet, [witness]::Bool=false)`

Check whether a set is contained in a polyhedral set, and if not, optionally compute a witness.

**Input**

`X`

– inner set`Y`

– outer polyhedral set`witness`

– (optional, default:`false`

) compute a witness if activated

**Output**

- If
`witness`

option is deactivated:`true`

iff $X ⊆ P$ - If
`witness`

option is activated:`(true, [])`

iff $X ⊆ P$`(false, v)`

iff $X ⊈ P$ and $v ∈ X \setminus P$

**Notes**

We require that `constraints_list(P)`

is available.

**Algorithm**

We check inclusion of `X`

in every constraint of `P`

.

`⊆(S::LazySet, H::AbstractHyperrectangle, [witness]::Bool=false)`

**Input**

`S`

– inner set`H`

– outer hyperrectangular set`witness`

– (optional, default:`false`

) compute a witness if activated

**Output**

- If
`witness`

option is deactivated:`true`

iff $S ⊆ H$ - If
`witness`

option is activated:`(true, [])`

iff $S ⊆ H$`(false, v)`

iff $S ⊈ H$ and $v ∈ S \setminus H$

**Algorithm**

```
⊆(H1::AbstractHyperrectangle, H2::AbstractHyperrectangle,
[witness]::Bool=false)
```

Check whether a given hyperrectangular set is contained in another hyperrectangular set, and if not, optionally compute a witness.

**Input**

`H1`

– inner hyperrectangular set`H2`

– outer hyperrectangular set`witness`

– (optional, default:`false`

) compute a witness if activated

**Output**

- If
`witness`

option is deactivated:`true`

iff $H1 ⊆ H2$ - If
`witness`

option is activated:`(true, [])`

iff $H1 ⊆ H2$`(false, v)`

iff $H1 ⊈ H2$ and $v ∈ H1 \setminus H2$

**Algorithm**

$H1 ⊆ H2$ iff $c_1 + r_1 ≤ c_2 + r_2 ∧ c_1 - r_1 ≥ c_2 - r_2$ iff $r_1 - r_2 ≤ c_1 - c_2 ≤ -(r_1 - r_2)$, where $≤$ is taken component-wise.

```
⊆(P::AbstractPolytope, S::LazySet, [witness]::Bool=false;
[algorithm]="constraints")
```

**Input**

`P`

– inner polytopic set`S`

– outer convex set`witness`

– (optional, default:`false`

) compute a witness if activated`algorithm`

– (optional, default:`"constraints"`

) algorithm for the inclusion check; available options are:`"constraints"`

, using the list of constraints of`S`

(requires that`S`

is polyhedral) and support-function evaluations of`S`

`"vertices"`

, using the list of vertices of`P`

and membership evaluations of`S`

**Output**

- If
`witness`

option is deactivated:`true`

iff $P ⊆ S$ - If
`witness`

option is activated:`(true, [])`

iff $P ⊆ S$`(false, v)`

iff $P ⊈ S$ and $v ∈ P \setminus S$

**Algorithm**

`"vertices"`

:

Since $S$ is convex, $P ⊆ S$ iff $v ∈ S$ for all vertices $v$ of $P$.

`⊆(X::LazySet, P::AbstractPolyhedron, [witness]::Bool=false)`

**Input**

`X`

– inner convex set`P`

– outer polyhedral set`witness`

– (optional, default:`false`

) compute a witness if activated

**Output**

- If
`witness`

option is deactivated:`true`

iff $X ⊆ P$ - If
`witness`

option is activated:`(true, [])`

iff $X ⊆ P$`(false, v)`

iff $X ⊈ P$ and $v ∈ P \setminus X$

**Algorithm**

For witness generation, we use a support vector in the first direction where the above check fails.

`⊆(S::AbstractSingleton, X::LazySet, [witness]::Bool=false)`

Check whether a given set with a single value is contained in another set, and if not, optionally compute a witness.

**Input**

`S`

– inner set with a single value`X`

– outer set`witness`

– (optional, default:`false`

) compute a witness if activated

**Output**

- If
`witness`

option is deactivated:`true`

iff $S ⊆ X$ - If
`witness`

option is activated:`(true, [])`

iff $S ⊆ X$`(false, v)`

iff $S ⊈ X$ and $v ∈ S \setminus X$

`⊆(Z::AbstractZonotope, H::AbstractHyperrectangle, [witness]::Bool=false)`

Check whether a zonotopic set is contained in a hyperrectangular set.

**Input**

`Z`

– inner zonotopic set`H`

– outer hyperrectangular set`witness`

– (optional, default:`false`

) compute a witness if activated (currently not supported)

**Output**

`true`

iff $Z ⊆ H$.

**Algorithm**

The algorithm is based on Lemma 3.1 in [1].

[1] Mitchell, I. M., Budzis, J., & Bolyachevets, A. *Invariant, viability and discriminating kernel under-approximation via zonotope scaling*. HSCC 2019.

`Base.:⊆`

— Function`⊆(S1::AbstractSingleton, S2::AbstractSingleton, witness::Bool=false)`

Check whether a given set with a single value is contained in another set with a single value, and if not, optionally compute a witness.

**Input**

`S1`

– inner set with a single value`S2`

– outer set with a single value`witness`

– (optional, default:`false`

) compute a witness if activated

**Output**

- If
`witness`

option is deactivated:`true`

iff $S1 ⊆ S2$ iff $S1 == S2$ - If
`witness`

option is activated:`(true, [])`

iff $S1 ⊆ S2$`(false, v)`

iff $S1 ⊈ S2$ and $v ∈ S1 \setminus S2$

`Base.:⊆`

— Function`⊆(B1::Ball2, B2::Ball2, [witness]::Bool=false)`

Check whether a ball in the 2-norm is contained in another ball in the 2-norm, and if not, optionally compute a witness.

**Input**

`B1`

– inner ball in the 2-norm`B2`

– outer ball in the 2-norm`witness`

– (optional, default:`false`

) compute a witness if activated

**Output**

- If
`witness`

option is deactivated:`true`

iff $B1 ⊆ B2$ - If
`witness`

option is activated:`(true, [])`

iff $B1 ⊆ B2$`(false, v)`

iff $B1 ⊈ B2$ and $v ∈ B1 \setminus B2$

**Algorithm**

$B1 ⊆ B2$ iff $‖ c_1 - c_2 ‖_2 + r_1 ≤ r_2$

`Base.:⊆`

— Function`⊆(B::Union{Ball2, Ballp}, S::AbstractSingleton, witness::Bool=false)`

Check whether a ball in the 2-norm or p-norm is contained in a set with a single value, and if not, optionally compute a witness.

**Input**

`B`

– inner ball in the 2-norm or p-norm`S`

– outer set with a single value`witness`

– (optional, default:`false`

) compute a witness if activated

**Output**

- If
`witness`

option is deactivated:`true`

iff $B ⊆ S$ - If
`witness`

option is activated:`(true, [])`

iff $B ⊆ S$`(false, v)`

iff $B ⊈ S$ and $v ∈ B \setminus S$

`Base.:⊆`

— Function`⊆(L::LineSegment, S::LazySet, witness::Bool=false)`

Check whether a line segment is contained in a convex set, and if not, optionally compute a witness.

**Input**

`L`

– inner line segment`S`

– outer convex set`witness`

– (optional, default:`false`

) compute a witness if activated

**Output**

- If
`witness`

option is deactivated:`true`

iff $L ⊆ S$ - If
`witness`

option is activated:`(true, [])`

iff $L ⊆ S$`(false, v)`

iff $L ⊈ S$ and $v ∈ L \setminus S$

**Algorithm**

Since $S$ is convex, $L ⊆ S$ iff $p ∈ S$ and $q ∈ S$, where $p, q$ are the end points of $L$.

`Base.:⊆`

— Function`⊆(X::LazySet, P::LazySet, [witness]::Bool=false)`

Check whether a set is contained in a polyhedral set, and if not, optionally compute a witness.

**Input**

`X`

– inner set`Y`

– outer polyhedral set`witness`

– (optional, default:`false`

) compute a witness if activated

**Output**

- If
`witness`

option is deactivated:`true`

iff $X ⊆ P$ - If
`witness`

option is activated:`(true, [])`

iff $X ⊆ P$`(false, v)`

iff $X ⊈ P$ and $v ∈ X \setminus P$

**Notes**

We require that `constraints_list(P)`

is available.

**Algorithm**

We check inclusion of `X`

in every constraint of `P`

.

`⊆(S::LazySet, H::AbstractHyperrectangle, [witness]::Bool=false)`

**Input**

`S`

– inner set`H`

– outer hyperrectangular set`witness`

– (optional, default:`false`

) compute a witness if activated

**Output**

- If
`witness`

option is deactivated:`true`

iff $S ⊆ H$ - If
`witness`

option is activated:`(true, [])`

iff $S ⊆ H$`(false, v)`

iff $S ⊈ H$ and $v ∈ S \setminus H$

**Algorithm**

```
⊆(P::AbstractPolytope, S::LazySet, [witness]::Bool=false;
[algorithm]="constraints")
```

**Input**

`P`

– inner polytopic set`S`

– outer convex set`witness`

– (optional, default:`false`

) compute a witness if activated`algorithm`

– (optional, default:`"constraints"`

) algorithm for the inclusion check; available options are:`"constraints"`

, using the list of constraints of`S`

(requires that`S`

is polyhedral) and support-function evaluations of`S`

`"vertices"`

, using the list of vertices of`P`

and membership evaluations of`S`

**Output**

- If
`witness`

option is deactivated:`true`

iff $P ⊆ S$ - If
`witness`

option is activated:`(true, [])`

iff $P ⊆ S$`(false, v)`

iff $P ⊈ S$ and $v ∈ P \setminus S$

**Algorithm**

`"vertices"`

:

Since $S$ is convex, $P ⊆ S$ iff $v ∈ S$ for all vertices $v$ of $P$.

`⊆(X::LazySet, P::AbstractPolyhedron, [witness]::Bool=false)`

**Input**

`X`

– inner convex set`P`

– outer polyhedral set`witness`

– (optional, default:`false`

) compute a witness if activated

**Output**

- If
`witness`

option is deactivated:`true`

iff $X ⊆ P$ - If
`witness`

option is activated:`(true, [])`

iff $X ⊆ P$`(false, v)`

iff $X ⊈ P$ and $v ∈ P \setminus X$

**Algorithm**

For witness generation, we use a support vector in the first direction where the above check fails.

`⊆(L::LineSegment, S::LazySet, witness::Bool=false)`

Check whether a line segment is contained in a convex set, and if not, optionally compute a witness.

**Input**

`L`

– inner line segment`S`

– outer convex set`witness`

– (optional, default:`false`

) compute a witness if activated

**Output**

- If
`witness`

option is deactivated:`true`

iff $L ⊆ S$ - If
`witness`

option is activated:`(true, [])`

iff $L ⊆ S$`(false, v)`

iff $L ⊈ S$ and $v ∈ L \setminus S$

**Algorithm**

Since $S$ is convex, $L ⊆ S$ iff $p ∈ S$ and $q ∈ S$, where $p, q$ are the end points of $L$.

`⊆(Z::AbstractZonotope, H::AbstractHyperrectangle, [witness]::Bool=false)`

Check whether a zonotopic set is contained in a hyperrectangular set.

**Input**

`Z`

– inner zonotopic set`H`

– outer hyperrectangular set`witness`

– (optional, default:`false`

) compute a witness if activated (currently not supported)

**Output**

`true`

iff $Z ⊆ H$.

**Algorithm**

The algorithm is based on Lemma 3.1 in [1].

[1] Mitchell, I. M., Budzis, J., & Bolyachevets, A. *Invariant, viability and discriminating kernel under-approximation via zonotope scaling*. HSCC 2019.

`Base.:⊆`

— Function`⊆(x::Interval, y::Interval, [witness]::Bool=false)`

Check whether an interval is contained in another interval.

**Input**

`x`

– inner interval`y`

– outer interval`witness`

– (optional, default:`false`

) compute a witness if activated

**Output**

`true`

iff $x ⊆ y$.

`Base.:⊆`

— Function`⊆(x::Interval, U::UnionSet, [witness]::Bool=false)`

Check whether an interval is contained in the union of two convex sets.

**Input**

`x`

– inner interval`U`

– outer union of two convex sets

**Output**

`true`

iff `x ⊆ U`

.

**Notes**

This implementation assumes that `U`

is a union of one-dimensional convex sets. Since these are equivalent to intervals, we convert to `Interval`

s.

**Algorithm**

Let $U = a ∪ b$ where $a$ and $b$ are intervals and assume that the lower bound of $a$ is to the left of $b$. If the lower bound of $x$ is to the left of $a$, we have a counterexample. Otherwise we compute the set difference $y = x \ a$ and check whether $y ⊆ b$ holds.

`Base.:⊆`

— Function`⊆(∅::EmptySet, X::LazySet, witness::Bool=false)`

Check whether the empty set is contained in another set.

**Input**

`∅`

– inner empty set`X`

– outer set`witness`

– (optional, default:`false`

) compute a witness if activated (ignored, just kept for interface reasons)

**Output**

`true`

.

`Base.:⊆`

— Function`⊆(X::LazySet, ∅::EmptySet, [witness]::Bool=false)`

Check whether a set is contained in the empty set.

**Input**

`X`

– inner set`∅`

– outer empty set`witness`

– (optional, default:`false`

) compute a witness if activated

**Output**

`true`

iff `X`

is empty.

**Algorithm**

We rely on `isempty(X)`

for the emptiness check and on `an_element(X)`

for witness production.

`Base.:⊆`

— Function`⊆(U::UnionSet, X::LazySet, [witness]::Bool=false)`

Check whether a union of two convex sets is contained in another set.

**Input**

`U`

– inner union of two convex sets`X`

– outer set`witness`

– (optional, default:`false`

) compute a witness if activated

**Output**

- If
`witness`

option is deactivated:`true`

iff $\text{U} ⊆ X$ - If
`witness`

option is activated:`(true, [])`

iff $\text{U} ⊆ X$`(false, v)`

iff $\text{U} \not\subseteq X$ and $v ∈ \text{U} \setminus X$

`Base.:⊆`

— Function`⊆(U::UnionSetArray, X::LazySet, [witness]::Bool=false)`

Check whether a union of a finite number of convex sets is contained in another set.

**Input**

`U`

– inner union of a finite number of convex sets`X`

– outer set`witness`

– (optional, default:`false`

) compute a witness if activated

**Output**

- If
`witness`

option is deactivated:`true`

iff $\text{U} ⊆ X$ - If
`witness`

option is activated:`(true, [])`

iff $\text{U} ⊆ X$`(false, v)`

iff $\text{U} \not\subseteq X$ and $v ∈ \text{U} \setminus X$

`Base.:⊆`

— Function`⊆(X::LazySet, U::Universe, [witness]::Bool=false)`

Check whether a set is contained in a universe.

**Input**

`X`

– inner set`U`

– outer universe`witness`

– (optional, default:`false`

) compute a witness if activated

**Output**

- If
`witness`

option is deactivated:`true`

- If
`witness`

option is activated:`(true, [])`

`Base.:⊆`

— Function`⊆(U::Universe, X::LazySet, [witness]::Bool=false)`

Check whether a universe is contained in another set, and otherwise optionally compute a witness.

**Input**

`U`

– inner universe`X`

– outer set`witness`

– (optional, default:`false`

) compute a witness if activated

**Output**

- If
`witness`

option is deactivated:`true`

iff $U ⊆ X$ - If
`witness`

option is activated:`(true, [])`

iff $U ⊆ X$`(false, v)`

iff $U \not\subseteq X$ and $v ∈ U \setminus X$

**Algorithm**

We fall back to `isuniversal(X)`

.

`Base.:⊆`

— Function`⊆(X::LazySet, C::Complement, [witness]::Bool=false)`

Check whether a set is contained in the complement of another set, and otherwise optionally compute a witness.

**Input**

`X`

– inner set`C`

– outer complement of a set`witness`

– (optional, default:`false`

) compute a witness if activated

**Output**

- If
`witness`

option is deactivated:`true`

iff $X ⊆ C$ - If
`witness`

option is activated:`(true, [])`

iff $X ⊆ C$`(false, v)`

iff $X \not\subseteq C$ and $v ∈ X \setminus C$

**Algorithm**

We fall back to `isdisjoint(X, C.X)`

, which can be justified as follows.

\[ X ⊆ Y^C ⟺ X ∩ Y = ∅\]

`Base.:⊆`

— Function```
⊆(X::CartesianProduct, Y::CartesianProduct, [witness]::Bool=false;
check_block_equality::Bool=true)
```

Check whether a Cartesian product of two sets is contained in another Cartesian product of two sets, and otherwise optionally compute a witness.

**Input**

`X`

– inner Cartesian product of two sets`Y`

– outer Cartesian product of two sets`witness`

– (optional, default:`false`

) compute a witness if activated`check_block_equality`

– (optional, default:`true`

) flag for checking that the block structure of the two sets is identical

**Output**

- If
`witness`

option is deactivated:`true`

iff $X ⊆ Y$ - If
`witness`

option is activated:`(true, [])`

iff $X ⊆ Y$`(false, v)`

iff $X \not\subseteq Y$ and $v ∈ X \setminus Y$

**Notes**

This algorithm requires that the two Cartesian products share the same block structure. If `check_block_equality`

is activated, we check this property and, if it does not hold, we use a fallback implementation based on conversion to constraint representation (assuming that the sets are polyhedral).

**Algorithm**

We check inclusion for each block of the Cartesian products.

For witness production, we obtain a witness in one of the blocks. We then construct a high-dimensional witness by obtaining any point in the other blocks (using `an_element`

) and concatenating these (lower-dimensional) points.

`Base.:⊆`

— Function```
⊆(X::CartesianProductArray, Y::CartesianProductArray, [witness]::Bool=false;
check_block_equality::Bool=true)
```

Check whether a Cartesian product of finitely many sets is contained in another Cartesian product of finitely many sets, and otherwise optionally compute a witness.

**Input**

`X`

– inner Cartesian product of finitely many sets`Y`

– outer Cartesian product of finitely many sets`witness`

– (optional, default:`false`

) compute a witness if activated`check_block_equality`

– (optional, default:`true`

) flag for checking that the block structure of the two sets is identical

**Output**

- If
`witness`

option is deactivated:`true`

iff $X ⊆ Y$ - If
`witness`

option is activated:`(true, [])`

iff $X ⊆ Y$`(false, v)`

iff $X \not\subseteq Y$ and $v ∈ X \setminus Y$

**Notes**

This algorithm requires that the two Cartesian products share the same block structure. If `check_block_equality`

is activated, we check this property and, if it does not hold, we use a fallback implementation based on conversion to constraint representation (assuming that the sets are polyhedral).

**Algorithm**

We check inclusion for each block of the Cartesian products.

For witness production, we obtain a witness in one of the blocks. We then construct a high-dimensional witness by obtaining any point in the other blocks (using `an_element`

) and concatenating these (lower-dimensional) points.

`Base.:⊆`

— Function`⊆(Z::AbstractZonotope, H::AbstractHyperrectangle, [witness]::Bool=false)`

Check whether a zonotopic set is contained in a hyperrectangular set.

**Input**

`Z`

– inner zonotopic set`H`

– outer hyperrectangular set`witness`

– (optional, default:`false`

) compute a witness if activated (currently not supported)

**Output**

`true`

iff $Z ⊆ H$.

**Algorithm**

The algorithm is based on Lemma 3.1 in [1].

*Invariant, viability and discriminating kernel under-approximation via zonotope scaling*. HSCC 2019.

`Base.:⊆`

— Function```
⊆(X::LazySet{N}, U::UnionSetArray, witness::Bool=false;
filter_redundant_sets::Bool=true) where {N}
```

Check whether a set is contained in a union of a finite number of sets.

**Input**

`X`

– inner set`U`

– outer union of a finite number of sets`witness`

– (optional, default:`false`

) compute a witness if activated`filter_redundant_sets`

– (optional, default:`true`

) ignore sets in`U`

that do not intersect with`X`

**Output**

`true`

iff $X ⊆ U$.

**Algorithm**

This implementation is general and successively removes parts from `X`

that are covered by the sets in the union $U$ using the `difference`

function. For the resulting subsets, this implementation relies on the methods `isdisjoint`

, `⊆`

, and `intersection`

.

As a preprocessing, this implementation checks if `X`

is contained in any of the sets in `U`

.

The `filter_redundant_sets`

option controls whether sets in `U`

that do not intersect with `X`

should be ignored.

## Strict subset check

`IntervalArithmetic.:⊂`

— Function`⊂(X::LazySet{N}, Y::LazySet, [witness]::Bool=false) where {N}`

Strict inclusion check of a set in another set.

**Input**

`X`

– first set`Y`

– second set`witness`

– (optional, default:`false`

) compute a witness if activated

**Output**

- If
`witness`

option is deactivated:`true`

iff $X ⊂ Y$ - If
`witness`

option is activated:`(true, v)`

iff $X ⊂ Y$ and $v ∈ Y \setminus X$`(false, [])`

iff not $X ⊂ Y$

**Algorithm**

We check inclusion of `X`

in `Y`

and then check inclusion of `Y`

in `X`

:

\[X ⊂ Y \Leftrightarrow X ⊆ Y \land ¬ (Y ⊆ X)\]