ThmDex – An index of mathematical definitions, results, and conjectures.
Set of symbols
Alphabet
Deduction system
Theory
Zermelo-Fraenkel set theory
Set
Collection of sets
Set union
Successor set
Definition D193
Inductive set
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}