The |`t operator could be used not only for topologies

[Glauco]

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

[Mario Carneiro]

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

--
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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/9cb56fe2-1b8e-4f27-b47d-057941fd085cn%40googlegroups.com.

[Benoit]

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

[Alexander van der Vekens]

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.

$c |`t $. $( Function returning a subspace . $)

    $( Function returning the subspace. For example, if  ` y ` is a topology, this is the subspace topology induced by ` y `
       and the set ` x ` .  (Contributed by FL, 20-Sep-2010.)  (Revised by
       Mario Carneiro, 1-May-2015.) $)
    df-rest $a |- |`t = ( j e. _V , x e. _V |->
      ran ( y e. j |-> ( y i^i x ) ) ) $.

Alexander

[Mario Carneiro]

On Sun, Apr 18, 2021 at 8:05 AM Benoit <benoit...@gmail.com> 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 <meta...@googlegroups.com> 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

[Benoit]

As for the statement: Mario above is right, so, if I get it right this time, one can prove

  |- ( ( X e. V /\ A C_ U. X ) -> U. ( X |`t A ) = A )

and

  |- ( ( X e. V /\ A e. W ) -> U. ( X |`t A ) = ( ( U. X ) i^i A ) )

As for the name: why not call |` the "elementwise intersection" and write in the comment: "if x is a family of sets, then ( x |` y ) is the family obtained from x where each member of x is intersected by y."

Benoît