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

Definition df-mrc 13767
 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 17098) and linear span (mrclsp 16020). A Moore closure operation is (1) extensive, i.e., for all subsets of the base set (mrcssid 13797), (2) isotone, i.e., implies that for all subsets and of the base set (mrcss 13796), and (3) idempotent, i.e., for all subsets of the base set (mrcidm 13799.) 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 13763 . 2 mrCls
2 vc . . 3
3 cmre 13762 . . . . 5 Moore
43crn 4838 . . . 4 Moore
54cuni 3975 . . 3 Moore
6 vx . . . 4
72cv 1648 . . . . . 6
87cuni 3975 . . . . 5
98cpw 3759 . . . 4
106cv 1648 . . . . . . 7
11 vs . . . . . . . 8
1211cv 1648 . . . . . . 7
1310, 12wss 3280 . . . . . 6
1413, 11, 7crab 2670 . . . . 5
1514cint 4010 . . . 4
166, 9, 15cmpt 4226 . . 3
172, 5, 16cmpt 4226 . 2 Moore
181, 17wceq 1649 1 mrCls Moore
 Colors of variables: wff set class This definition is referenced by:  fnmrc  13787  mrcfval  13788
 Copyright terms: Public domain W3C validator