Commit 2022-07-19 03:29 58d7431d

View on Github →

refactor(set_theory/zfc): Union → sUnion (#15352) The current Union definitions more closely match set.sUnion. We also change the notation to match. See Zulip.

Estimated changes

Modified src/set_theory/zfc.lean

deleted def Class.Union

deleted theorem Class.Union_hom

modified def Class.iota

added def Class.sUnion

added theorem Class.sUnion_hom

deleted def Set.Union

deleted theorem Set.Union_lem

deleted theorem Set.Union_singleton

modified theorem Set.choice_is_func

deleted theorem Set.mem_Union

added theorem Set.mem_sUnion

added def Set.sUnion

added theorem Set.sUnion_lem

added theorem Set.sUnion_singleton

deleted def pSet.Union

deleted theorem pSet.mem_Union

added theorem pSet.mem_sUnion

added def pSet.sUnion