ordinal): von Neumann hierarchy
#18521

Open

feat(set_theory/zfc/ordinal): von Neumann hierarchy #18521

vihdzp wants to merge 10 commits into master from vn_hierarchy

Update basic.lean

fad72042

generalize universes

caede292

more lemmas on transitive sets

3172cdf5

Add universe comment

2aa37797

Merge branch 'zfc_range' into vn_hierarchy

03c67299

von neumann hierarchy

49972062

Merge branch 'master' into vn_hierarchy

68ec00b9

Merge branch 'zfc_transitive_powerset' into vn_hierarchy

92f22848

golf

95c94550

vihdzp added awaiting-review

vihdzp requested a review from

astrainfinita 2 years ago

vihdzp assigned

digama0 2 years ago

mathlib-dependent-issues-bot added blocked-by-other-PR

mathlib-dependent-issues-bot removed blocked-by-other-PR

Merge branch 'master' into vn_hierarchy

260b3601

vihdzp commented on 2023-03-29

eric-wieser added not-too-late

Reviewers

astrainfinita

Assignees

digama0

Labels

awaiting-review not-too-late

Milestone

No milestone