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

Definition df-mrc 13804
 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 17135) and linear span (mrclsp 16057). A Moore closure operation is (1) extensive, i.e., for all subsets of the base set (mrcssid 13834), (2) isotone, i.e., implies that for all subsets and of the base set (mrcss 13833), and (3) idempotent, i.e., for all subsets of the base set (mrcidm 13836.) 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 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 Moore
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-mrc
StepHypRef Expression
1 cmrc 13800 . 2 mrCls
2 vc . . 3
3 cmre 13799 . . . . 5 Moore
43crn 4871 . . . 4 Moore
54cuni 4007 . . 3 Moore
6 vx . . . 4
72cv 1651 . . . . . 6
87cuni 4007 . . . . 5
98cpw 3791 . . . 4
106cv 1651 . . . . . . 7
11 vs . . . . . . . 8
1211cv 1651 . . . . . . 7
1310, 12wss 3312 . . . . . 6
1413, 11, 7crab 2701 . . . . 5
1514cint 4042 . . . 4
166, 9, 15cmpt 4258 . . 3
172, 5, 16cmpt 4258 . 2 Moore
181, 17wceq 1652 1 mrCls Moore
 Colors of variables: wff set class This definition is referenced by:  fnmrc  13824  mrcfval  13825
 Copyright terms: Public domain W3C validator