Inaccessible cardinal

Remarks

The cardinal $\aleph_0$ satisfies clauses 2 and 3, since a union of finitely many finite sets is finite and $2^n$ is finite; it fails only clause 1. The cardinal $\aleph_1$ is regular but not inaccessible: it fails clause 3, since $2^{\aleph_0} \ge \aleph_1$. Every inaccessible cardinal is weakly inaccessible, and under the generalized continuum hypothesis the two notions agree. If $\kappa$ is inaccessible, then $V_\kappa$, the set of sets of rank less than $\kappa$, is a model of ZFC. By Gödel's second incompleteness theorem, ZFC therefore cannot prove that an inaccessible cardinal exists, if ZFC is consistent. In Mathlib the notion is Cardinal.IsInaccessible.