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.
