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/CAFXXJStZ%2BN%3DEa%3D%3Di0QRNx%3D%2B%2Bf%3DF4uhYE8cVcyKDpAi%3D1pwarmA%40mail.gmail.com.
