Theorems · Definition · logic and foundations

ZFSet.range

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

The range of a type-indexed family of sets.

Defined in

Mathlib.SetTheory.ZFC.Basic

Cited by

6 results in Mathlib

Foundations

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

Assumes

Small