Theorems · Theorem · logic and foundations
ZFSet.iSup_card_le_card_iUnion
∀ {α : Type u} [inst : Small.{v, u} α] {f : α → ZFSet.{v}}, ⨆ i, (f i).card ≤ (ZFSet.iUnion fun i => f i).card- Defined in
- Mathlib.SetTheory.ZFC.Cardinal
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 77 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Small
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites13
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Set.Elemproof · cited by 7,166
- Set.rangeproof · cited by 4,705
- Cardinalstatement and proof · cited by 2,598
- iSupstatement and proof · cited by 2,415
- Cardinal.mkproof · cited by 942
- Smallstatement and proof · cited by 369
- ZFSetstatement and proof · cited by 259
- Cardinal.bddAbove_of_smallproof · cited by 37
- Cardinal.lift_iSupproof · cited by 16
- ZFSet.cardstatement and proof · cited by 16
- ZFSet.iUnionstatement · cited by 10
- ZFSet.cardinalMk_coe_sortproof · cited by 7
Cited by1
Results whose statement or proof uses this declaration.
- ZFSet.card_vonNeumannproof · cited by 0