mathlib

d7feae34 - feat(set_theory/zfc/basic): induction principle for sets (#18324)

feat(set_theory/zfc/basic): induction principle for sets (#18324) If every subset of a class is a member, the class is universal. This will help us establish that the von Neumann hierarchy exhausts sets later on.