VonNeumann

📁 Source: Mathlib/SetTheory/ZFC/VonNeumann.lean

Statistics

Metric	Count
Definitions `termV_`, `vonNeumann`	2
Theorems `card_le_card_vonNeumann`, `toZFSet_subset_vonNeumann`, `card_vonNeumann`, `exists_mem_vonNeumann`, `iUnion_vonNeumann`, `isTransitive_vonNeumann`, `mem_vonNeumann`, `mem_vonNeumann'`, `mem_vonNeumann_of_subset`, `mem_vonNeumann_succ`, `rank_vonNeumann`, `subset_vonNeumann`, `subset_vonNeumann_self`, `vonNeumann_inj`, `vonNeumann_injective`, `vonNeumann_mem_of_lt`, `vonNeumann_mem_vonNeumann_iff`, `vonNeumann_of_isSuccPrelimit`, `vonNeumann_strictMono`, `vonNeumann_subset_of_le`, `vonNeumann_subset_vonNeumann_iff`, `vonNeumann_succ`, `vonNeumann_zero`	23
Total	25

Ordinal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_le_card_vonNeumann` 📖	mathematical	—	`Cardinal` `Cardinal.instLE` `card` `ZFSet.card` `ZFSet.vonNeumann`	—	`card_toZFSet` `ZFSet.card_mono` `toZFSet_subset_vonNeumann`
`toZFSet_subset_vonNeumann` 📖	mathematical	—	`ZFSet` `ZFSet.instHasSubset` `toZFSet` `ZFSet.vonNeumann`	—	`rank_toZFSet`

ZFSet

Definitions

Name	Category	Theorems
`termV_` 📖	CompOp	—
`vonNeumann` 📖	CompOp	22 math math: `subset_vonNeumann`, `vonNeumann_inj`, `vonNeumann_subset_vonNeumann_iff`, `vonNeumann_subset_of_le`, `exists_mem_vonNeumann`, `mem_vonNeumann'`, `vonNeumann_mem_vonNeumann_iff`, `vonNeumann_strictMono`, `subset_vonNeumann_self`, `iUnion_vonNeumann`, `vonNeumann_injective`, `vonNeumann_zero`, `Ordinal.toZFSet_subset_vonNeumann`, `mem_vonNeumann_succ`, `mem_vonNeumann`, `Ordinal.card_le_card_vonNeumann`, `vonNeumann_mem_of_lt`, `vonNeumann_of_isSuccPrelimit`, `rank_vonNeumann`, `isTransitive_vonNeumann`, `vonNeumann_succ`, `card_vonNeumann`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_vonNeumann` 📖	mathematical	—	`card` `vonNeumann` `Cardinal.preBeth`	—	`vonNeumann_zero` `card_empty` `Cardinal.preBeth_zero` `vonNeumann_succ` `Nat.instAtLeastTwoHAddOfNat` `card_powerset` `Cardinal.preBeth_succ` `Cardinal.preBeth_limit` `Order.IsSuccLimit.isSuccPrelimit` `Ordinal.small_Iio` `vonNeumann_of_isSuccPrelimit` `LE.le.antisymm'` `iSup_card_le_card_iUnion` `Cardinal.lift_le` `LE.le.trans` `lift_card_iUnion_le_sum_card` `Eq.le` `Cardinal.sum_eq_lift_iSup_of_lift_mk_le_lift_iSup` `Ordinal.mk_Iio_ordinal` `Cardinal.lift_aleph0` `Ordinal.aleph0_le_card` `Ordinal.omega0_le_of_isSuccLimit` `Cardinal.lift_lift` `Eq.not_lt` `Cardinal.card_ord` `LE.le.trans_lt` `Ordinal.card_le_card_vonNeumann` `LT.lt.trans_le` `Cardinal.cantor` `le_ciSup` `Cardinal.bddAbove_of_small` `small_range` `Order.IsSuccLimit.succ_lt` `LE.le.trans_lt'` `Cardinal.ord_card_le` `Cardinal.ord_strictMono`
`exists_mem_vonNeumann` 📖	mathematical	—	`ZFSet` `instMembership` `vonNeumann`	—	`mem_vonNeumann_succ`
`iUnion_vonNeumann` 📖	mathematical	—	`Set.iUnion` `ZFSet` `Ordinal` `Class.ofSet` `vonNeumann` `Class.univ`	—	`Class.eq_univ_of_forall` `Set.mem_iUnion` `exists_mem_vonNeumann`
`isTransitive_vonNeumann` 📖	mathematical	—	`IsTransitive` `vonNeumann`	—	`Ordinal.small_Iio` `vonNeumann.eq_1` `IsTransitive.iUnion` `IsTransitive.powerset`
`mem_vonNeumann` 📖	mathematical	—	`ZFSet` `instMembership` `vonNeumann` `Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `Ordinal.partialOrder` `rank`	—	`LE.le.trans_lt` `le_refl`
`mem_vonNeumann'` 📖	mathematical	—	`ZFSet` `instMembership` `vonNeumann` `Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `Ordinal.partialOrder` `instHasSubset`	—	`Ordinal.small_Iio` `vonNeumann.eq_1`
`mem_vonNeumann_of_subset` 📖	—	`ZFSet` `instHasSubset` `instMembership` `vonNeumann`	—	—	`mem_vonNeumann` `LE.le.trans_lt` `rank_mono`
`mem_vonNeumann_succ` 📖	mathematical	—	`ZFSet` `instMembership` `vonNeumann` `Order.succ` `Ordinal` `PartialOrder.toPreorder` `Ordinal.partialOrder` `Ordinal.instSuccOrder` `rank`	—	`Ordinal.instNoMaxOrder`
`rank_vonNeumann` 📖	mathematical	—	`rank` `vonNeumann`	—	`le_antisymm` `subset_vonNeumann` `subset_refl` `instReflSubset` `le_of_forall_lt` `rank_lt_of_mem` `vonNeumann_mem_of_lt`
`subset_vonNeumann` 📖	mathematical	—	`ZFSet` `instHasSubset` `vonNeumann` `Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `Ordinal.partialOrder` `rank`	—	—
`subset_vonNeumann_self` 📖	mathematical	—	`ZFSet` `instHasSubset` `vonNeumann` `rank`	—	—
`vonNeumann_inj` 📖	mathematical	—	`vonNeumann`	—	`vonNeumann_injective`
`vonNeumann_injective` 📖	mathematical	—	`Ordinal` `ZFSet` `vonNeumann`	—	`StrictMono.injective` `vonNeumann_strictMono`
`vonNeumann_mem_of_lt` 📖	mathematical	`Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `Ordinal.partialOrder`	`ZFSet` `instMembership` `vonNeumann`	—	`Ordinal.small_Iio` `vonNeumann.eq_1` `subset_refl` `instReflSubset`
`vonNeumann_mem_vonNeumann_iff` 📖	mathematical	—	`ZFSet` `instMembership` `vonNeumann` `Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `Ordinal.partialOrder`	—	`rank_vonNeumann`
`vonNeumann_of_isSuccPrelimit` 📖	mathematical	`Order.IsSuccPrelimit` `Ordinal` `Preorder.toLT` `PartialOrder.toPreorder` `Ordinal.partialOrder`	`vonNeumann` `iUnion` `Set.Elem` `Set.Iio` `Ordinal.small_Iio` `Set` `Set.instMembership`	—	`ext` `Ordinal.small_Iio` `Order.IsSuccPrelimit.lt_iff_exists_lt`
`vonNeumann_strictMono` 📖	mathematical	—	`StrictMono` `Ordinal` `ZFSet` `PartialOrder.toPreorder` `Ordinal.partialOrder` `instPartialOrder` `vonNeumann`	—	`strictMono_of_le_iff_le`
`vonNeumann_subset_of_le` 📖	mathematical	`Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `Ordinal.partialOrder`	`ZFSet` `instHasSubset` `vonNeumann`	—	`instReflSubset` `isTransitive_vonNeumann` `vonNeumann_mem_of_lt` `LE.le.eq_or_lt`
`vonNeumann_subset_vonNeumann_iff` 📖	mathematical	—	`ZFSet` `instHasSubset` `vonNeumann` `Ordinal` `Preorder.toLE` `PartialOrder.toPreorder` `Ordinal.partialOrder`	—	`rank_vonNeumann`
`vonNeumann_succ` 📖	mathematical	—	`vonNeumann` `Order.succ` `Ordinal` `PartialOrder.toPreorder` `Ordinal.partialOrder` `Ordinal.instSuccOrder` `powerset`	—	`ext` `mem_vonNeumann` `mem_powerset` `subset_vonNeumann` `Order.lt_succ_iff` `Ordinal.instNoMaxOrder`
`vonNeumann_zero` 📖	mathematical	—	`vonNeumann` `Ordinal` `Ordinal.zero` `ZFSet` `instEmptyCollection`	—	`eq_empty` `Ordinal.canonicallyOrderedAdd`

---

← Back to Index