Intersection of Auxiliary Relations is Auxiliary Relation

From ProofWiki
Jump to navigation Jump to search

Theorem

Let $L = \left({S, \vee, \preceq}\right)$ be a bounded below join semilattice.

Let $\mathcal F$ be a non-empty set of auxiliary relations on $S$.


Then

$\bigcap \mathcal F$ is auxiliary relation.


Proof

By definition of non-empty set:

$\exists \mathcal R: \mathcal R \in \mathcal F$

We will prove that

$\forall x, y \in S: \left({x, y}\right) \in \bigcap \mathcal F \implies x \preceq y$

Let $x, y \in S$ such that

$\left({x, y}\right) \in \bigcap \mathcal F$

By definition of intersection:

$\left({x, y}\right) \in \mathcal R$

Thus by definition of auxiliary relation:

$x \preceq y$

$\Box$

We will prove that

$\forall x, y, z, u \in S: x \preceq y \land \left({y, z}\right) \in \bigcap \mathcal F \land z \preceq u \implies \left({x, u}\right) \in \bigcap \mathcal F$

Let $x, y, z, u \in S$ such that

$x \preceq y \land \left({y, z}\right) \in \bigcap \mathcal F \land z \preceq u$

By definition of intersection:

$\forall r \in \mathcal F: \left({y, z}\right) \in r$

By definition of auxiliary relation:

$\forall r \in \mathcal F: \left({x, u}\right) \in r$

Thus by definition of intersection:

$\left({x, u}\right) \in \bigcap \mathcal F$

$\Box$

We will prove that

$\forall x, y, z \in S: \left({x, z}\right) \in \bigcap \mathcal F \land \left({y, z}\right) \in \bigcap \mathcal F \implies \left({x \vee y, z}\right) \in \bigcap \mathcal F$

Let $x, y, z \in S$ such that

$\left({x, z}\right) \in \bigcap \mathcal F \land \left({y, z}\right) \in \bigcap \mathcal F$

By definition of intersection:

$\forall r \in \mathcal F: \left({x, z}\right) \in r \land \left({y, z}\right) \in r$

By definition of auxiliary relation:

$\forall r \in \mathcal F: \left({x \vee y, z}\right) \in r$

Thus by definition of intersection:

$\left({x \vee y, z}\right) \in \bigcap \mathcal F$

$\Box$

By definition of auxiliary relation:

$\forall x \in S: \forall r \in \mathcal F: \left({\bot, x}\right) \in r$

Thus by definition of intersection:

$\forall x \in S: \left({\bot, x}\right) \in \bigcap \mathcal F$

Thus by definition:

$\bigcap \mathcal F$ is auxiliary relation.

$\blacksquare$


Sources