On Sun, Apr 18, 2021 at 8:05 AM Benoit <[email protected]> wrote:
> Why not the hypothesis-free form > |- ( ( J e. V /\ A C_ U. J ) -> A = U. ( J |`t A ) ) > That is, you inline the definition of X. Theorems using this result might > be a bit longer, but the statement looks leaner. > That's a useful theorem, but it doesn't replace the existing one, which is intended for the (not so) special case where A is defined to be U. J. Well, we're moving away from this style anyway in favor of extensible structure versions, where you don't have to worry about reconstructing the base set from one of the fields. > Also: is the antecedent J \in V necessary ? I think that it is not, since > if J is a proper class, one has empty = empty in the consequent. I am not > sure how things are coded in set.mm, but I think that the union of a > proper class is the empty set. > The union of a proper class is (potentially) a proper class, for example univ. So the theorem is false without the assumption. > Maybe that even the antecedent A \subseteq \bigcup J is unnecessary, and > one has > |- U. ( J |`t A ) ) = (U. J) \cap A > This might be more general but it's less useful, because now you have to rewrite quite a bit to get back to the original version. (It also still needs the assumption on J being a set, and this version also needs A to be a set.) On Sun, Apr 18, 2021 at 8:28 AM 'Alexander van der Vekens' via Metamath < [email protected]> wrote: > Since |`t is defined in Part 7 BASIC STRUCTURES, and not in PART 12 BASIC > TOPOLOGY, I think this operator can be used also in other contexts (by the > way, the group identity element 0g is defined in the same section "7.1.3 > Definition of the structure product", although groups and monoids are > defined in Part 10 at first). > > Maybe |`t can be called "subspace operator", and the comments could be > adjusted, as Glauco suggested, e.g. > While I think it would be fine to use the term "subspace operator" if only by convention, there are lots of things that are called subspaces in mathematics and this operator only applies to structures that involve sets of sets. For example vector subspaces, metric subspaces, Hilbert subspaces and so on; none of these use this operator to form the subspace. It would be more appropriate to apply this term to df-ress, which is indended for taking subspaces in all kinds of structures. Mario -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSub1mHedLxBXo19EV6j%3DNSmOyP7vSqyg%2BAPNM01UxU3eA%40mail.gmail.com.
