Theorems · Definition · logic and foundations

ZFSet.iUnion

{α : Type u_1} → [Small.{u, u_1} α] → (α → ZFSet.{u}) → ZFSet.{u}

Indexed union of a family of ZFC sets. Uses ⋃ notation, scoped under the ZFSet namespace.

Defined in

Mathlib.SetTheory.ZFC.Basic

Cited by

10 results in Mathlib

Foundations

Depth 17 from the axioms · uses Classical.choice, Quot.sound

Assumes

Small