ThmDex – An index of mathematical definitions, results, and conjectures.
Formulation F9335 on D193: Inductive set
F9335
Formulation 0
Let $\emptyset$ be the D13: Empty set.
A D11: Set $x$ is an inductive set if and only if
(1) \begin{equation} \emptyset \in x \end{equation}
(2) \begin{equation} \forall \, y \in x : y \cup \{ y \} \in x \end{equation}