Commit 2022-07-19 03:29 58d7431d

View on Github →

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

Estimated changes

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