Fix misc markup (#3248)

Author: tirix

set.mm

@@ -150740,7 +150740,7 @@ computer programs (as last() or lastChar()), the terminology used for
     $( There is a unique word having the length of a given word increased by 1
        with the given word as prefix if there is a unique symbol which extends
        the given word.  (Contributed by Alexander van der Vekens, 6-Oct-2018.)
-       (Revised by AV, 21-Jan-2022.)  (Revised by AV, 10-May-2020.)  (Proof
+       (Revised by AV, 21-Jan-2022.)  (Revised by AV, 10-May-2022.)  (Proof
        shortened by AV, 13-Oct-2022.) $)
     reuccatpfxs1v $p |- ( ( W e. Word V /\ A. x e. X ( x e. Word V
                                            /\ ( # ` x ) = ( ( # ` W ) + 1 ) ) )
@@ -321580,7 +321580,7 @@ need not be complete (for instance if the given set is infinite
 
     $( Define a function generating the real Euclidean spaces of finite
        dimension.  The case ` n = 0 ` corresponds to a space of dimension 0,
-       that is, limited to a neutral element (see ~ehl0 ).  Members of this
+       that is, limited to a neutral element (see ~ ehl0 ).  Members of this
        family of spaces are Hilbert spaces, as shown in - ehlhl .  (Contributed
        by Thierry Arnoux, 16-Jun-2019.) $)
     df-ehl $a |- EEhil = ( n e. NN0 |-> ( RR^ ` ( 1 ... n ) ) ) $.
@@ -412773,7 +412773,7 @@ closed walk p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n)=p(0) as
     $( The set of closed walks of a fixed length ` N ` as words over the set of
        vertices in a graph ` G ` .  (Contributed by Alexander van der Vekens,
        20-Mar-2018.)  (Revised by AV, 24-Apr-2021.)  (Revised by AV,
-       22-Mar-2021.) $)
+       22-Mar-2022.) $)
     clwwlkn $p |- ( N ClWWalksN G ) = { w e. ( ClWWalks ` G ) |
                                         ( # ` w ) = N } $=
       ( vn vg cn0 wcel cvv wa cclwwlkn co cv chash wceq cclwwlk crab wn c0 wral
@@ -412791,7 +412791,7 @@ closed walk p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n)=p(0) as
     $d G w $.  $d N w $.  $d W w $.
     $( A word over the set of vertices representing a closed walk of a fixed
        length.  (Contributed by Alexander van der Vekens, 15-Mar-2018.)
-       (Revised by AV, 24-Apr-2021.)  (Revised by AV, 22-Mar-2021.) $)
+       (Revised by AV, 24-Apr-2021.)  (Revised by AV, 22-Mar-2022.) $)
     isclwwlkn $p |- ( W e. ( N ClWWalksN G )
                       <-> ( W e. ( ClWWalks ` G ) /\ ( # ` W ) = N ) ) $=
       ( vw cv chash cfv wceq cclwwlk cclwwlkn co fveqeq2 clwwlkn elrab2 ) DEZFG
@@ -616119,7 +616119,7 @@ fixed reference functional determined by this vector (corresponding to
   the result of ` ( A .+ B ) ` only needs to be a complex number).
 
   The natural numbers are especially amenable to axiom reductions, as the set
-  ` NN ` is the recursive set ` { 1 , ( 1 + 1 ) , ( ( 1 + 1 ) + 1 ) }` , etc.,
+  ` NN ` is the recursive set ` { 1 , ( 1 + 1 ) , ( ( 1 + 1 ) + 1 ) } ` , etc.,
   i.e. the set of numbers formed by only additions of 1.  The digits 2 through
   9 are defined so that they expand into additions of 1.  This makes adding
   natural numbers conveniently only require the rearrangement of parentheses,
@@ -712170,18 +712170,18 @@ description binder (inverted iota). $)
        ordinarily contains ` x ` as a free variable.  Our definition is
        meaningful only when there is exactly one ` x ` such that ` ph ` is true
        (see ~ aiotaval ); otherwise, it is not a set (see ~ aiotaexb ), or even
-       more concrete, it is the universe ` _V ` (see ~aiotavb ).  Since this is
-       an alternative for ~df-iota , we call this symbol ` iota' ` _alternate
-       iota_ in the following.
+       more concrete, it is the universe ` _V ` (see ~ aiotavb ).  Since this
+       is an alternative for ~ df-iota , we call this symbol ` iota' `
+       _alternate iota_ in the following.
 
        The advantage of this definition is the clear distinguishability of the
        defined and undefined cases: the alternate iota over a wff is defined
        iff it is a set (see ~ aiotaexb ).  With the original definition, there
        is no corresponding theorem ` ( E! x ph <-> ( iota x ph ) =/= (/) ) ` ,
        because ` (/) ` can be a valid unique set satisfying a wff (see, for
-       example, ~iota0def ).  Only the right to left implication would hold,
-       see (negated) ~iotanul .  For defined cases, however, both definitions
-       ~df-iota and ~df-aiota are equivalent, see ~ reuaiotaiota .  (Proposed
+       example, ~ iota0def ).  Only the right to left implication would hold,
+       see (negated) ~ iotanul .  For defined cases, however, both definitions
+       ~ df-iota and ~ df-aiota are equivalent, see ~ reuaiotaiota .  (Proposed
        by BJ, 13-Aug-2022.)  (Contributed by AV, 24-Aug-2022.) $)
     df-aiota $a |- ( iota' x ph ) = |^| { y | { x | ph } = { y } } $.
 
@@ -713831,7 +713831,7 @@ Alternative definitions of function values (2)
   (see ~ dfatafv2eqfv ).
 
   With this definition the following intuitive equivalence holds:
-  ` ( F defAt A <-> ( F '''' A ) e. ran F ) `, see ~dfatafv2rnb .
+  ` ( F defAt A <-> ( F '''' A ) e. ran F ) `, see ~ dfatafv2rnb .
 
   An interesting question would be if ` ( F `` A ) ` could be replaced by
   ` ( F ''' A ) ` in most of the theorems based on function values.  If we look
@@ -722327,7 +722327,7 @@ and specializations for simple hypergraphs ( ~ isomushgr ) and simple
   definition in [Bollobas] p. 3).  It is shown that the isomorphy relation for
   graphs is an equivalence relation ( ~ isomgrref , ~ isomgrsym , ~ isomgrtr ).
   Fianlly, isomorphic graphs with different representations are studied
-  ( ~strisomgrop , ~ ushrisomgr ).
+  ( ~ strisomgrop , ~ ushrisomgr ).
 
   Maybe more important than graph isomorphy is the notion of graph isomorphism,
   which can be defined as in ~ df-grisom .  Then ` A IsomGr B <-> `