Subset relation


THEOREM    \(A \subseteq B \Leftrightarrow (\forall x : x \in A \Rightarrow x \in B)\)
subset_iff: (?A \(\subseteq\) ?B) = (\(\forall\)t. t \(\in\) ?A \(\longrightarrow\) t \(\in\) ?B)

Proof unavailable

THEOREM   

The subset relation is reflexive.

$$A \subseteq A$$

Proof available

THEOREM   

The subset relation is antisymmetric.

$$A \subseteq B \wedge B \subseteq A \Rightarrow A = B$$

Proof available

THEOREM   

The subset relation is transitive.

$$A \subseteq B \wedge B \subseteq C \Rightarrow A \subseteq C$$

Proof available

THEOREM   

The empty set is a subset of every set.

$$\emptyset \subseteq A$$

Proof available

THEOREM   

Every set is a subset of the universal set.

$$A \subseteq \mathcal{U}$$

Proof available

Proper supersets