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
--
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/14a79950-e586-4bc9-8301-76f766aa64bdn%40googlegroups.com.
