mathlib3

800d3d45 - feat(set_theory/zfc/basic): better docs on `univ_not_mem_univ` (#18234)

feat(set_theory/zfc/basic): better docs on `univ_not_mem_univ` (#18234) This theorem is somewhat odd, but phrases a very important result: there is no ZFC universal set. The new docs better clarify this.