Yury G. Kudryashov (May 20 2020 at 21:50):
Is there any reason to (a) use
x ∈ s instead of
(x) (hx : p x) in
bUnion etc? (b) assume that the inner expression does not depend on
Mario Carneiro (May 20 2020 at 22:38):
If you generalize them enough it will become "Union, twice"
Last updated: Aug 03 2023 at 10:10 UTC