Algebra of sets

From Automated Assistance for Formal Reasoning

Jump to: navigation, search

The algebra of sets governs the basic properties and laws of sets, as well as common operations that can be performed on sets. Many of these are supported by the static context.

[edit] Sets

An expression is specified to be a set using the corresponding predicate.

Introduce $X,Y,Z$ .

Assume $X$ is a set, $Y$ is a set, $Z$ is a set.

Specific sets have corresponding predicates.

Introduce $A,B,C$ .

Assume $A$ is the empty set and $B$ is a non-empty set.

Assert $A$ is empty, $A$ is a set, $A = \emptyset$ , $B \neq \emptyset$ .

[edit] Subset relations

The typical subset relations are supported.

Assert if $X \subseteq Y$ and $Y \subseteq Z$ then $X \subseteq Z$ .

Assert if $X \subset Y$ and $Y \subset Z$ then $X \subset Z$ .

Assert $A \subseteq B$ .

[edit] Common set operations

Assert $\emptyset \cap X = X \cap \emptyset = \emptyset$ .

Assert $\emptyset \cup X = X \cup \emptyset = X$ .

Assert $X \cap (Y \cap Z) = (X \cap Y) \cap Z$ .

Assert $X \cap Y \subseteq X$ , $X \subseteq X \cup Y$ .

Assert if $X \subseteq Z$ and $Y \subseteq Z$ then $X \cup Y \subseteq Z$ .

Retrieved from "http://www.aartifact.org/wiki/index.php/Algebra_of_sets"

Views

Personal tools

Log in

Search

Toolbox