MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-mrc Unicode version

Definition df-mrc 13485
Description: Define the Moore closure of a generating set, which is the smallest closed set containing all generating elements. Definition of Moore closure in [Schechter] p. 79. This generalizes topological closure (mrccls 16812) and linear span (mrclsp 15742).

A Moore closure operation  N is (1) extensive, i.e.,  x  C_  ( N `  x ) for all subsets  x of the base set (mrcssid 13515), (2) isotone, i.e.,  x  C_  y implies that  ( N `
 x )  C_  ( N `  y ) for all subsets  x and  y of the base set (mrcss 13514), and (3) idempotent, i.e.,  ( N `  ( N `  x )
)  =  ( N `
 x ) for all subsets  x of the base set (mrcidm 13517.) Operators satisfying these three properties are in bijective correspondence with Moore collections, so these properties may be used to give an alternate characterization of a Moore collection by providing a closure operation  N on the set of subsets of a given base set which satisfies (1), (2), and (3); the closed sets can be recovered as those sets which equal their closures (Section 4.5 in [Schechter] p. 82.) (Contributed by Stefan O'Rear, 31-Jan-2015.) (Revised by David Moews, 1-May-2017.)

Assertion
Ref Expression
df-mrc  |- mrCls  =  ( c  e.  U. ran Moore  |->  ( x  e.  ~P U. c  |->  |^| { s  e.  c  |  x  C_  s } ) )
Distinct variable group:    s, c, x

Detailed syntax breakdown of Definition df-mrc
StepHypRef Expression
1 cmrc 13481 . 2  class mrCls
2 vc . . 3  set  c
3 cmre 13480 . . . . 5  class Moore
43crn 4689 . . . 4  class  ran Moore
54cuni 3828 . . 3  class  U. ran Moore
6 vx . . . 4  set  x
72cv 1622 . . . . . 6  class  c
87cuni 3828 . . . . 5  class  U. c
98cpw 3626 . . . 4  class  ~P U. c
106cv 1622 . . . . . . 7  class  x
11 vs . . . . . . . 8  set  s
1211cv 1622 . . . . . . 7  class  s
1310, 12wss 3153 . . . . . 6  wff  x  C_  s
1413, 11, 7crab 2548 . . . . 5  class  { s  e.  c  |  x 
C_  s }
1514cint 3863 . . . 4  class  |^| { s  e.  c  |  x 
C_  s }
166, 9, 15cmpt 4078 . . 3  class  ( x  e.  ~P U. c  |-> 
|^| { s  e.  c  |  x  C_  s } )
172, 5, 16cmpt 4078 . 2  class  ( c  e.  U. ran Moore  |->  ( x  e.  ~P U. c  |-> 
|^| { s  e.  c  |  x  C_  s } ) )
181, 17wceq 1623 1  wff mrCls  =  ( c  e.  U. ran Moore  |->  ( x  e.  ~P U. c  |->  |^| { s  e.  c  |  x  C_  s } ) )
Colors of variables: wff set class
This definition is referenced by:  fnmrc  13505  mrcfval  13506
  Copyright terms: Public domain W3C validator