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.
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. Maybe that even the antecedent A \subseteq \bigcup J is unnecessary, and one has |- U. ( J |`t A ) ) = (U. J) \cap A Benoît On Sunday, April 18, 2021 at 2:43:37 AM UTC+2 [email protected] wrote: > I don't think its use is necessarily limited to topologies, but that is > the original and primary use case, so I don't see a huge issue with the > name. It will work as long as it operates on a set of subsets of X of which > X must be a member. That includes topologies, set-filters, subgroups and > other moore algebras, sigma algebras and algebras of sets, but not > set-ideals, which lack the "contains X" property. > > I think restuni5 should replace restuni. > > Mario > > On Sat, Apr 17, 2021 at 4:50 PM Glauco <[email protected]> wrote: > >> The definition or the |`t operator is topology agnostic, but all comments >> refer to it as the subspace topology operator. >> >> I need a subspace operator for sigma-algebras and |`t is just perfect >> (I've already used it for a number of not published theorems) >> >> Furthermore, it looks like it would be perfect to define subspaces for >> other "structures" of sets (where difference, union and intersection are >> the only "operators" taken into account) >> >> For instance, algebras of sets, semialgebras of sets, rings of sets and >> semirings of sets are good candidates: I've not investigated these >> additional "structures", but it looks like |`t would construct subspaces >> (please, don't quote me on this, I've not written definitions/theorems to >> be sure about it). >> >> So, my question is, how should I proceed? (please, consider that this is >> a KEY concept in order to define partially defined measurable functions, >> that's at the core of [Fremlin1] development of integration) >> >> I'm happily going on with |`t in my definition of subspace sigma-algebra: >> of course, I'm a bit concerned, because throughout all set.mm , COMMENTS >> refer to |`t as being related to topologies. >> >> I'm using comments like the following: >> The underlying set of a subspace induced by the ` |``t ` operator. The >> result can be applied, for instance, to topologies and sigma-algebras. >> >> Here's an example of restuni5, a theorem (not published, yet) that >> generalizes restuni (restuni5 is "structure" agnostic) >> >> restuni.1 $e |- X = U. J $. >> restuni $p |- ( ( J e. Top /\ A C_ X ) -> A = U. ( J |`t A ) ) $= >> >> restuni5.1 $e |- X = U. J $. >> restuni5 $p |- ( ( J e. V /\ A C_ X ) -> A = U. ( J |`t A ) ) $= >> >> >> Please, let me know how I should proceed: should I keep using |`t for >> sigma-algebras too? >> >> >> Thanks in advance >> Glauco >> >> -- >> 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/9cb56fe2-1b8e-4f27-b47d-057941fd085cn%40googlegroups.com >> >> <https://groups.google.com/d/msgid/metamath/9cb56fe2-1b8e-4f27-b47d-057941fd085cn%40googlegroups.com?utm_medium=email&utm_source=footer> >> . >> > -- 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/86f2ff16-ffc1-4380-b93d-b23f856ccc08n%40googlegroups.com.
