Mathlib Map

Theorems · Theorem · logic and foundations

ZFSet.subset_iUnion

∀ {α : Type u_1} [inst : Small.{u, u_1} α] (f : α → ZFSet.{u}) (i : α), f i ⊆ ZFSet.iUnion fun i => f i
Defined in
Mathlib.SetTheory.ZFC.Basic
Cited by
1 results in Mathlib
Foundations
Depth 24 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
Small
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

ZFSet.rank_iUnion · cited by 0ZFSet.rank_iUnionSmall · cited by 369SmallZFSet · cited by 259ZFSetZFSet.iUnion · cited by 10ZFSet.iUnionZFSet.subset_iUnionCITED BYCITES

Cites3

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Smallstatement and proof · cited by 369
  • ZFSetstatement and proof · cited by 259
  • ZFSet.iUnionstatement · cited by 10

Cited by1

Results whose statement or proof uses this declaration.