
TL;DR
This paper introduces a local operation on finite binary relations that preserves or increases the number of Galois-closed sets and can precisely control the VC-dimension and the count of closed sets.
Contribution
It demonstrates the existence of a specific subrelation that maximizes Galois-closed sets for given VC-dimension and ground set sizes.
Findings
Existence of subrelations with at least half the Galois-closed sets.
Construction of relations with specified VC-dimension and maximum Galois-closed sets.
Theoretical bounds on the number of Galois-closed sets for given parameters.
Abstract
For a finite binary relation, we show a local operation which does not decrease its number of (Galois-)closed sets and eventually increases its (Vapnik-Chervonenkis)-dimension. Specifically, we show that there always exist a pair of elements, one belonging to each ground set, such that the subrelation not relating any of those elements has at least half of the Galois-closed sets. As a consequence, for each triple (n,m,k) there exists a binary relation with VC-dimension precisely k and maximum number of Galois-closed sets, such maximum being over all binary relations having ground sets with precisely n and m elements.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsSemantic Web and Ontologies
Rich subcontexts
Alexandre Albano
(as of July 30)
1 Introduction
It is not well understood which effects small changes to a formal context have on its concept lattice (for the definition of said structure, as well as basics on Formal Concept Analysis, we refer the reader to [GW99]). Deleting an object (or an attribute) may, for example, reduce the number of concepts by up to 50%. What happens if we delete both, an object and an attribute? The extreme case is that the number of concepts divides by four. This indeed happens, for instance, if one deletes an incident object-attribute pair in a contranominal scale. Even with the restriction that the deleted pair be non-incident, it is possible that the number of concepts gets reduced to one third of the original number. In this paper, we show that there always exists an object-attribute pair such that the number of concepts at most halves after its deletion. As an application, this result establishes a weak form of a conjecture involving number of concepts of a formal context and contranominal scales found as subcontexts.
2 Motivation
In what follows, we present two aspects of our main motivation to investigate the question. A few elementary defininitions are introduced and related work is shown as well.
2.1 Local changes to a formal context and their effects
Understanding how a lattice changes after some part of its associated context gets modified is of great interest to comprehend how a conceptual system evolves. Quite a few problems of this nature were already posed and solved, but many questions still remain. Solutions to those kind of problems may, for instance, provide insights for lattice drawing algorithms.
Removing an object and a non-incident attribute can lead to a loss of more than 50% of the concepts. Indeed, consider the standard context of the three element chain (that is, the unique two-by-two reduced Ferrers context). It is clear that the removal of its object which has no attributes, along with the removal of the empty column results in a one-by-one full context, which has only one concept.
For a less trivial example which results even in reduced subcontexts, consider the formal context present in Figure 1. Its lattice has elements and, when object and attribute both are removed, a (reduced) sub-context with only 7 concepts remains. In contrast, removing and results in a sub-context with 9 concepts (which is reduced as well).
So let be finite, and let us call a sub-context
[TABLE]
rich, if
[TABLE]
As a first contribution, we ask
Question 1**.**
Does there always exist a choice of a non-incident object/attribute pair in a non-trivial finite context , such that is rich?
The aforementioned question is closely related to another problem which was studied by the author during his investigations of contranominal scale free contexts with as many concepts as possible:
Question 2**.**
Does there always exist a choice of an object/attribute pair in a context , such that , where
[TABLE]
has at least as many concepts as the original?
It is not surprising that both questions are actually equivalent:
Proposition 1**.**
A subcontext is rich if and only if is a suitable choice to answer Question 2 affirmatively.
Proof.
Let be a non-incident pair. The concept lattice of the context described in Question 2 is clearly , where denotes direct sum of contexts. The associated concept lattice is therefore the direct product of and , which has at least as many elements as whenever is rich. Conversely, if (as defined in the description of Question 2) has at least as many concepts as , then clearly the removal of from yields a context with at least half of the concepts of and in which is a full column. The removal of a full column does not change the number of concepts (and neither changes the structure of the lattice). ∎
We now illustrate in which mathematical context Question 2 came to our attention.
2.2 Extremal results relating number of concepts and contranominal scales
A context of the form will be called a contranominal scale of size . Albano and Chornomaz showed the following result relating number of concepts and contranominal scales, where an operation which they call “doubling” was employed:
Theorem 1**.**
An arbitrary formal context with exactly objects and no contranominal scale of size as a subcontext may have up to concepts (but no more). The associated lattices achieving this bound are precisely consecutive doublings of chains inside boolean lattices.
It is natural that further results in this direction try to include the number of attributes as a piece of additional information: How many concepts may a formal context with objects, attributes and no contranominal scale of size have? Is that bound achievable? If so, what can be said about contexts (or associated lattices) which achieve this bound? A first step towards that is the following:
Conjecture**.**
Amongst the contexts with objects, attributes and no contranominal scale of size , every context with maximum number of concepts has a contranominal scale of size as a subcontext.
We show in Section 4 that a positive answer to Question 2 is able to establish, without substantial additional effort, the following weaker form of the conjecture:
Claim 1**.**
Amongst the contexts with objects, attributes and no contranominal scale of size , there exists one context with maximum number of concepts which has a contranominal scale of size as a subcontext.
The aforementioned result and questions belong to the framework of extremal combinatorics and may be rewritten in graph-theoretic language as well. Citing Béla Bollobás: “Extremal graph theory, in its strictest sense, is a branch of graph theory developed and loved by Hungarians.” [Bol78]. It is therefore no surprise that a very important milestone of that area was established by another Hungarian:
Theorem 2** (Turán, 1941).**
An arbitrary simple graph with exactly vertices and no clique of size may have up to edges (but no more). The graphs achieving this bound are precisely the complete, balanced, -partite graphs.
The nature of the questions answered by results like Theorems 1 and 2 are analogous. More abstractly, Bollobás describes in [Bol78] the following typical setting in an extremal graph theory problem:
Setting:
Given a property and an invariant for a class of graphs, we wish to determine the least value for which every graph in with has property . The graphs in without property and are called the extremal graphs for the problem.
Theorem 1 and the mentioned conjecture are instances of the described setting above. In both, denotes the property of having a contranominal scale of some given size, while corresponds to the number of concepts of a context. They differ, however, in what gets defined to be: the conjecture asks about the interaction between and in a subclass of the class treated in Theorem 1, since that theorem is indifferent about the number of attributes that a context has. At this point we start to digress and shall now turn back to rich subcontexts.
3 Existence of rich subcontexts
We set some notation. For a formal context , and such that , we define , where is defined as in Question 2. Derivation will be denoted by writing the incidence relation in a superscript, and we only use to denote derivation in a context obtained by the operation . To attack Question 2, we make use of the following:
Definition** (mixed generator).**
Let be fixed. A set is called a -mixed generator (of the extent ) if, for every , both implications below hold:
[TABLE]
Note that -mixed generators are minimal generators and that -mixed generators are extents. We ocasionally refer to a -mixed generator simply by mixed generator or by mixgen if there is no possibility for ambiguity. Proposition 2 describes which mixed generators are extents as well with arbitrary .
Proposition 2**.**
Let be a context and be a -mixed generator. Then, is an extent if and only if .
Proof.
The direct implication is clear since whenever is an extent. For the converse, we prove the contraposition. Suppose that is not an extent and take . Note that implies . Condition of the definition of mixgens forces, therefore, that . Because of , it holds that . ∎
We are particularly interested in the case when is the set of objects not having some fixed attribute, that is, when . For this reason, we set the notation m^{\leavevmode\hbox to10.36pt{\vbox to10.36pt{\pgfpicture\makeatletter\hbox{\hskip 5.17923pt\lower-5.17923pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{}\pgfsys@moveto{4.97923pt}{0.0pt}\pgfsys@curveto{4.97923pt}{2.74998pt}{2.74998pt}{4.97923pt}{0.0pt}{4.97923pt}\pgfsys@curveto{-2.74998pt}{4.97923pt}{-4.97923pt}{2.74998pt}{-4.97923pt}{0.0pt}\pgfsys@curveto{-4.97923pt}{-2.74998pt}{-2.74998pt}{-4.97923pt}{0.0pt}{-4.97923pt}\pgfsys@curveto{2.74998pt}{-4.97923pt}{4.97923pt}{-2.74998pt}{4.97923pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.7989pt}{-2.39166pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\hskip 1.13809pt\scriptsize\!I}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}=G\setminus m^{I}. Note that, in this case, the set is precisely the set of objects whose derivation are changed by the operation .
Proposition 3**.**
Let be a context, R=m^{\leavevmode\hbox to10.36pt{\vbox to10.36pt{\pgfpicture\makeatletter\hbox{\hskip 5.17923pt\lower-5.17923pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{}\pgfsys@moveto{4.97923pt}{0.0pt}\pgfsys@curveto{4.97923pt}{2.74998pt}{2.74998pt}{4.97923pt}{0.0pt}{4.97923pt}\pgfsys@curveto{-2.74998pt}{4.97923pt}{-4.97923pt}{2.74998pt}{-4.97923pt}{0.0pt}\pgfsys@curveto{-4.97923pt}{-2.74998pt}{-2.74998pt}{-4.97923pt}{0.0pt}{-4.97923pt}\pgfsys@curveto{2.74998pt}{-4.97923pt}{4.97923pt}{-2.74998pt}{4.97923pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.7989pt}{-2.39166pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\hskip 1.13809pt\scriptsize\!I}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}} for some attribute and be a set with . Then, is a -mixed generator if and only if is an extent.
Proof.
Suppose that is a mixed generator. Therefore, for every . Moreover, and R=m^{\leavevmode\hbox to10.36pt{\vbox to10.36pt{\pgfpicture\makeatletter\hbox{\hskip 5.17923pt\lower-5.17923pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{}\pgfsys@moveto{4.97923pt}{0.0pt}\pgfsys@curveto{4.97923pt}{2.74998pt}{2.74998pt}{4.97923pt}{0.0pt}{4.97923pt}\pgfsys@curveto{-2.74998pt}{4.97923pt}{-4.97923pt}{2.74998pt}{-4.97923pt}{0.0pt}\pgfsys@curveto{-4.97923pt}{-2.74998pt}{-2.74998pt}{-4.97923pt}{0.0pt}{-4.97923pt}\pgfsys@curveto{2.74998pt}{-4.97923pt}{4.97923pt}{-2.74998pt}{4.97923pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.7989pt}{-2.39166pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\hskip 1.13809pt\scriptsize\!I}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}} clearly imply for every . Combining both yields for every , i.e., is an extent. For the converse, suppose that is an extent. Since , the set fulfills trivially condition of mixgens. Condition is likewise fulfilled by because of for every . ∎
An easy but handy fact is the following:
Proposition 4**.**
A set which is a mixed generator and an extent is always the unique mixed generator of itself.
Proof.
Let be -mixed generators with . Since is an extent, it follows that . A proper containment would contradict the fact that is a mixed generator. Similarly, would imply the existence of an object with and , yielding and contradicting the fact that is a mixed generator. ∎
Consider the context present in Figure 1 and set R=m^{\leavevmode\hbox to10.36pt{\vbox to10.36pt{\pgfpicture\makeatletter\hbox{\hskip 5.17923pt\lower-5.17923pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{}\pgfsys@moveto{4.97923pt}{0.0pt}\pgfsys@curveto{4.97923pt}{2.74998pt}{2.74998pt}{4.97923pt}{0.0pt}{4.97923pt}\pgfsys@curveto{-2.74998pt}{4.97923pt}{-4.97923pt}{2.74998pt}{-4.97923pt}{0.0pt}\pgfsys@curveto{-4.97923pt}{-2.74998pt}{-2.74998pt}{-4.97923pt}{0.0pt}{-4.97923pt}\pgfsys@curveto{2.74998pt}{-4.97923pt}{4.97923pt}{-2.74998pt}{4.97923pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.7989pt}{-2.39166pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\hskip 1.13809pt\scriptsize\!I}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}=\{g,h\}. (The reader is invited to contemplate Figure 2 for an alternative representation of that context). The set (we omit sometimes braces and commas) may be verified as being a mixed generator, since the removal of any element belonging to causes its closure (equivalently, its derivation) to change and there is no element in which can be added to without changing its closure. Note that is not an extent. Similarly, one may observe that is an extent but not a mixed generator. Lastly, is both an extent and a mixed generator, whereas the set is neither an extent nor a mixed generator.
In Figure 2, objects in correspond to ellipses whereas objects not in correspond to closed polygonal curves with rounded corners. A mixed generator corresponds to an exact cover of vertices which is minimal with respect to ellipses and maximal with respect to polygonal curves.
The following proposition will be needed later, in the particular case when an object/attribute pair “splits” the concepts of a context: that is, is the only object without attribute , while is the only attribute which does not have. Similarly with what was done with attributes, we define g^{\leavevmode\hbox to10.36pt{\vbox to10.36pt{\pgfpicture\makeatletter\hbox{\hskip 5.17923pt\lower-5.17923pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{}\pgfsys@moveto{4.97923pt}{0.0pt}\pgfsys@curveto{4.97923pt}{2.74998pt}{2.74998pt}{4.97923pt}{0.0pt}{4.97923pt}\pgfsys@curveto{-2.74998pt}{4.97923pt}{-4.97923pt}{2.74998pt}{-4.97923pt}{0.0pt}\pgfsys@curveto{-4.97923pt}{-2.74998pt}{-2.74998pt}{-4.97923pt}{0.0pt}{-4.97923pt}\pgfsys@curveto{2.74998pt}{-4.97923pt}{4.97923pt}{-2.74998pt}{4.97923pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.7989pt}{-2.39166pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\hskip 1.13809pt\scriptsize\!I}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}=M\setminus g^{I}. For other incidence relations we write, for example, g^{\leavevmode\hbox to10.36pt{\vbox to10.36pt{\pgfpicture\makeatletter\hbox{\hskip 5.17923pt\lower-5.17923pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{}\pgfsys@moveto{4.97923pt}{0.0pt}\pgfsys@curveto{4.97923pt}{2.74998pt}{2.74998pt}{4.97923pt}{0.0pt}{4.97923pt}\pgfsys@curveto{-2.74998pt}{4.97923pt}{-4.97923pt}{2.74998pt}{-4.97923pt}{0.0pt}\pgfsys@curveto{-4.97923pt}{-2.74998pt}{-2.74998pt}{-4.97923pt}{0.0pt}{-4.97923pt}\pgfsys@curveto{2.74998pt}{-4.97923pt}{4.97923pt}{-2.74998pt}{4.97923pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.26314pt}{-2.39166pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\hskip 1.13809pt\scriptsize\!J}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}.
Proposition 5**.**
Let be a mixed generator. If is an object such that , g^{\leavevmode\hbox to10.36pt{\vbox to10.36pt{\pgfpicture\makeatletter\hbox{\hskip 5.17923pt\lower-5.17923pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{}\pgfsys@moveto{4.97923pt}{0.0pt}\pgfsys@curveto{4.97923pt}{2.74998pt}{2.74998pt}{4.97923pt}{0.0pt}{4.97923pt}\pgfsys@curveto{-2.74998pt}{4.97923pt}{-4.97923pt}{2.74998pt}{-4.97923pt}{0.0pt}\pgfsys@curveto{-4.97923pt}{-2.74998pt}{-2.74998pt}{-4.97923pt}{0.0pt}{-4.97923pt}\pgfsys@curveto{2.74998pt}{-4.97923pt}{4.97923pt}{-2.74998pt}{4.97923pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.7989pt}{-2.39166pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\hskip 1.13809pt\scriptsize\!I}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\neq\emptyset and g^{\leavevmode\hbox to10.36pt{\vbox to10.36pt{\pgfpicture\makeatletter\hbox{\hskip 5.17923pt\lower-5.17923pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{}\pgfsys@moveto{4.97923pt}{0.0pt}\pgfsys@curveto{4.97923pt}{2.74998pt}{2.74998pt}{4.97923pt}{0.0pt}{4.97923pt}\pgfsys@curveto{-2.74998pt}{4.97923pt}{-4.97923pt}{2.74998pt}{-4.97923pt}{0.0pt}\pgfsys@curveto{-4.97923pt}{-2.74998pt}{-2.74998pt}{-4.97923pt}{0.0pt}{-4.97923pt}\pgfsys@curveto{2.74998pt}{-4.97923pt}{4.97923pt}{-2.74998pt}{4.97923pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.7989pt}{-2.39166pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\hskip 1.13809pt\scriptsize\!I}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\cap h^{\leavevmode\hbox to10.36pt{\vbox to10.36pt{\pgfpicture\makeatletter\hbox{\hskip 5.17923pt\lower-5.17923pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{}\pgfsys@moveto{4.97923pt}{0.0pt}\pgfsys@curveto{4.97923pt}{2.74998pt}{2.74998pt}{4.97923pt}{0.0pt}{4.97923pt}\pgfsys@curveto{-2.74998pt}{4.97923pt}{-4.97923pt}{2.74998pt}{-4.97923pt}{0.0pt}\pgfsys@curveto{-4.97923pt}{-2.74998pt}{-2.74998pt}{-4.97923pt}{0.0pt}{-4.97923pt}\pgfsys@curveto{2.74998pt}{-4.97923pt}{4.97923pt}{-2.74998pt}{4.97923pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.7989pt}{-2.39166pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\hskip 1.13809pt\scriptsize\!I}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}=\emptyset for every , then is a mixed generator.
Proof.
Let and suppose that . Because is a mixed generator and , it follows that and, since , we have as well that , which is equivalent to . Now, suppose that . If , then it is clear that . Otherwise, we have certainly that and, since is a mixed generator, one necessarily has that there exists an attribute such that n\in h^{\leavevmode\hbox to10.36pt{\vbox to10.36pt{\pgfpicture\makeatletter\hbox{\hskip 5.17923pt\lower-5.17923pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{}\pgfsys@moveto{4.97923pt}{0.0pt}\pgfsys@curveto{4.97923pt}{2.74998pt}{2.74998pt}{4.97923pt}{0.0pt}{4.97923pt}\pgfsys@curveto{-2.74998pt}{4.97923pt}{-4.97923pt}{2.74998pt}{-4.97923pt}{0.0pt}\pgfsys@curveto{-4.97923pt}{-2.74998pt}{-2.74998pt}{-4.97923pt}{0.0pt}{-4.97923pt}\pgfsys@curveto{2.74998pt}{-4.97923pt}{4.97923pt}{-2.74998pt}{4.97923pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.7989pt}{-2.39166pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\hskip 1.13809pt\scriptsize\!I}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}} and, as a consequence, it holds that . Moreover, which implies . Thus, , which is equivalent to and establishes condition of the definition. ∎
Let be a formal context. A representative system of mixed generators is a family of subsets such that each is a mixed generator and is an injection from into . If the closure mapping is surjective as well, we call a complete representative system of mixed generators. For brevity we shall write only complete system of mixed generators.
Example:
Setting R=m^{\leavevmode\hbox to10.36pt{\vbox to10.36pt{\pgfpicture\makeatletter\hbox{\hskip 5.17923pt\lower-5.17923pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{}\pgfsys@moveto{4.97923pt}{0.0pt}\pgfsys@curveto{4.97923pt}{2.74998pt}{2.74998pt}{4.97923pt}{0.0pt}{4.97923pt}\pgfsys@curveto{-2.74998pt}{4.97923pt}{-4.97923pt}{2.74998pt}{-4.97923pt}{0.0pt}\pgfsys@curveto{-4.97923pt}{-2.74998pt}{-2.74998pt}{-4.97923pt}{0.0pt}{-4.97923pt}\pgfsys@curveto{2.74998pt}{-4.97923pt}{4.97923pt}{-2.74998pt}{4.97923pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.7989pt}{-2.39166pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\hskip 1.13809pt\scriptsize\!I}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}} in the context of the Figures 1 and 2 one has that the set family
[TABLE]
is a complete system of mixed generators.
For Propositions 6, 7 and 8, an arbitrary context and an object/attribute pair , with are to be considered; furthermore, denotes . Proposition 6 shows that a mixed generator in is halfway from being a mixed generator in : in that context, always fulfills condition of the definition.
Proposition 6**.**
Let R=m^{\leavevmode\hbox to10.36pt{\vbox to10.36pt{\pgfpicture\makeatletter\hbox{\hskip 5.17923pt\lower-5.17923pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{}\pgfsys@moveto{4.97923pt}{0.0pt}\pgfsys@curveto{4.97923pt}{2.74998pt}{2.74998pt}{4.97923pt}{0.0pt}{4.97923pt}\pgfsys@curveto{-2.74998pt}{4.97923pt}{-4.97923pt}{2.74998pt}{-4.97923pt}{0.0pt}\pgfsys@curveto{-4.97923pt}{-2.74998pt}{-2.74998pt}{-4.97923pt}{0.0pt}{-4.97923pt}\pgfsys@curveto{2.74998pt}{-4.97923pt}{4.97923pt}{-2.74998pt}{4.97923pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.7989pt}{-2.39166pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\hskip 1.13809pt\scriptsize\!I}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}} and let be a -mixed generator in . Then, for every with it holds that , where denotes derivation in . In particular, if , then is a -mixed generator in .
Proof.
Let . The fact that is a mixgen in implies . Hence, one has that , which is equivalent to h^{\leavevmode\hbox to10.36pt{\vbox to10.36pt{\pgfpicture\makeatletter\hbox{\hskip 5.17923pt\lower-5.17923pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{}\pgfsys@moveto{4.97923pt}{0.0pt}\pgfsys@curveto{4.97923pt}{2.74998pt}{2.74998pt}{4.97923pt}{0.0pt}{4.97923pt}\pgfsys@curveto{-2.74998pt}{4.97923pt}{-4.97923pt}{2.74998pt}{-4.97923pt}{0.0pt}\pgfsys@curveto{-4.97923pt}{-2.74998pt}{-2.74998pt}{-4.97923pt}{0.0pt}{-4.97923pt}\pgfsys@curveto{2.74998pt}{-4.97923pt}{4.97923pt}{-2.74998pt}{4.97923pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.7989pt}{-2.39166pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\hskip 1.13809pt\scriptsize\!I}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\cap S^{I}\neq\emptyset. Now, implies h^{\leavevmode\hbox to10.36pt{\vbox to10.36pt{\pgfpicture\makeatletter\hbox{\hskip 5.17923pt\lower-5.17923pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{}\pgfsys@moveto{4.97923pt}{0.0pt}\pgfsys@curveto{4.97923pt}{2.74998pt}{2.74998pt}{4.97923pt}{0.0pt}{4.97923pt}\pgfsys@curveto{-2.74998pt}{4.97923pt}{-4.97923pt}{2.74998pt}{-4.97923pt}{0.0pt}\pgfsys@curveto{-4.97923pt}{-2.74998pt}{-2.74998pt}{-4.97923pt}{0.0pt}{-4.97923pt}\pgfsys@curveto{2.74998pt}{-4.97923pt}{4.97923pt}{-2.74998pt}{4.97923pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.7989pt}{-2.39166pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\hskip 1.13809pt\scriptsize\!I}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}=h^{\leavevmode\hbox to10.36pt{\vbox to10.36pt{\pgfpicture\makeatletter\hbox{\hskip 5.17923pt\lower-5.17923pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{}\pgfsys@moveto{4.97923pt}{0.0pt}\pgfsys@curveto{4.97923pt}{2.74998pt}{2.74998pt}{4.97923pt}{0.0pt}{4.97923pt}\pgfsys@curveto{-2.74998pt}{4.97923pt}{-4.97923pt}{2.74998pt}{-4.97923pt}{0.0pt}\pgfsys@curveto{-4.97923pt}{-2.74998pt}{-2.74998pt}{-4.97923pt}{0.0pt}{-4.97923pt}\pgfsys@curveto{2.74998pt}{-4.97923pt}{4.97923pt}{-2.74998pt}{4.97923pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.26314pt}{-2.39166pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\hskip 1.13809pt\scriptsize\!J}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}} and this, together with the fact that , yields h^{\leavevmode\hbox to10.36pt{\vbox to10.36pt{\pgfpicture\makeatletter\hbox{\hskip 5.17923pt\lower-5.17923pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{}\pgfsys@moveto{4.97923pt}{0.0pt}\pgfsys@curveto{4.97923pt}{2.74998pt}{2.74998pt}{4.97923pt}{0.0pt}{4.97923pt}\pgfsys@curveto{-2.74998pt}{4.97923pt}{-4.97923pt}{2.74998pt}{-4.97923pt}{0.0pt}\pgfsys@curveto{-4.97923pt}{-2.74998pt}{-2.74998pt}{-4.97923pt}{0.0pt}{-4.97923pt}\pgfsys@curveto{2.74998pt}{-4.97923pt}{4.97923pt}{-2.74998pt}{4.97923pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.26314pt}{-2.39166pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\hskip 1.13809pt\scriptsize\!J}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\cap S^{J}\neq\emptyset. That is equivalent to . ∎
The reader is maybe aware of the fact that minimal generators form a downset: the removal of any element of a minimal generator yields another minimal generator. For mixed generators this is clearly not the case but, as expected, the same phenomenon happens when one removes elements which belong to . Indeed, we have the proposition below.
Proposition 7**.**
For every -mixed generator and every , it holds that is a mixed generator. In particular if R=m^{\leavevmode\hbox to10.36pt{\vbox to10.36pt{\pgfpicture\makeatletter\hbox{\hskip 5.17923pt\lower-5.17923pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{}\pgfsys@moveto{4.97923pt}{0.0pt}\pgfsys@curveto{4.97923pt}{2.74998pt}{2.74998pt}{4.97923pt}{0.0pt}{4.97923pt}\pgfsys@curveto{-2.74998pt}{4.97923pt}{-4.97923pt}{2.74998pt}{-4.97923pt}{0.0pt}\pgfsys@curveto{-4.97923pt}{-2.74998pt}{-2.74998pt}{-4.97923pt}{0.0pt}{-4.97923pt}\pgfsys@curveto{2.74998pt}{-4.97923pt}{4.97923pt}{-2.74998pt}{4.97923pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.7989pt}{-2.39166pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\hskip 1.13809pt\scriptsize\!I}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}, then is a mixed generator in both contexts, and . Moreover, is an extent in and, therefore, its unique mixed generator in that context.
Proof.
Set so that and . First we prove that, if the condition of mixed generators were not valid for , then it would also not be valid for the set . Suppose, therefore, that there exists with . Therefore, we have that . Now, regarding condition of mixed generators, take with . Observe that together with , and imply . Since is a mixed generator, we have that , which means that there exists an attribute n\in h^{\leavevmode\hbox to10.36pt{\vbox to10.36pt{\pgfpicture\makeatletter\hbox{\hskip 5.17923pt\lower-5.17923pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{}\pgfsys@moveto{4.97923pt}{0.0pt}\pgfsys@curveto{4.97923pt}{2.74998pt}{2.74998pt}{4.97923pt}{0.0pt}{4.97923pt}\pgfsys@curveto{-2.74998pt}{4.97923pt}{-4.97923pt}{2.74998pt}{-4.97923pt}{0.0pt}\pgfsys@curveto{-4.97923pt}{-2.74998pt}{-2.74998pt}{-4.97923pt}{0.0pt}{-4.97923pt}\pgfsys@curveto{2.74998pt}{-4.97923pt}{4.97923pt}{-2.74998pt}{4.97923pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.7989pt}{-2.39166pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\hskip 1.13809pt\scriptsize\!I}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}} with . Hence, . The three final claims (which require R=m^{\leavevmode\hbox to10.36pt{\vbox to10.36pt{\pgfpicture\makeatletter\hbox{\hskip 5.17923pt\lower-5.17923pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{}\pgfsys@moveto{4.97923pt}{0.0pt}\pgfsys@curveto{4.97923pt}{2.74998pt}{2.74998pt}{4.97923pt}{0.0pt}{4.97923pt}\pgfsys@curveto{-2.74998pt}{4.97923pt}{-4.97923pt}{2.74998pt}{-4.97923pt}{0.0pt}\pgfsys@curveto{-4.97923pt}{-2.74998pt}{-2.74998pt}{-4.97923pt}{0.0pt}{-4.97923pt}\pgfsys@curveto{2.74998pt}{-4.97923pt}{4.97923pt}{-2.74998pt}{4.97923pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.7989pt}{-2.39166pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\hskip 1.13809pt\scriptsize\!I}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}) come from Propositions 6, 3 and 4. ∎
For a moment, suppose that is finite and let denote a complete system of m^{\leavevmode\hbox to10.36pt{\vbox to10.36pt{\pgfpicture\makeatletter\hbox{\hskip 5.17923pt\lower-5.17923pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{}\pgfsys@moveto{4.97923pt}{0.0pt}\pgfsys@curveto{4.97923pt}{2.74998pt}{2.74998pt}{4.97923pt}{0.0pt}{4.97923pt}\pgfsys@curveto{-2.74998pt}{4.97923pt}{-4.97923pt}{2.74998pt}{-4.97923pt}{0.0pt}\pgfsys@curveto{-4.97923pt}{-2.74998pt}{-2.74998pt}{-4.97923pt}{0.0pt}{-4.97923pt}\pgfsys@curveto{2.74998pt}{-4.97923pt}{4.97923pt}{-2.74998pt}{4.97923pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.7989pt}{-2.39166pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\hskip 1.13809pt\scriptsize\!I}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}-mixed generators in . Our goal is to find a sufficient condition for , and the strategy to arrive at that shall be to reuse as much mixed generators from in as possible. Aiming this, we establish now what is necessary and sufficient for a mixed generator in not to be a mixed generator in . As an example, let denote the context of Figures 1 and 2 and consider the context , which is depicted in Figure 3. Observe that , which means that is not111Because . Notice that the set is not, in any sense, “updated”. a mixed generator in . Moreover, notice that has the following three properties: first, it does not contain . Second, its intersection with has cardinality one. Lastly, the derivation in (and in ) of equals . Proposition 8 shows that those properties are characteristic.
Proposition 8**.**
Let R=m^{\leavevmode\hbox to10.36pt{\vbox to10.36pt{\pgfpicture\makeatletter\hbox{\hskip 5.17923pt\lower-5.17923pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{}\pgfsys@moveto{4.97923pt}{0.0pt}\pgfsys@curveto{4.97923pt}{2.74998pt}{2.74998pt}{4.97923pt}{0.0pt}{4.97923pt}\pgfsys@curveto{-2.74998pt}{4.97923pt}{-4.97923pt}{2.74998pt}{-4.97923pt}{0.0pt}\pgfsys@curveto{-4.97923pt}{-2.74998pt}{-2.74998pt}{-4.97923pt}{0.0pt}{-4.97923pt}\pgfsys@curveto{2.74998pt}{-4.97923pt}{4.97923pt}{-2.74998pt}{4.97923pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.7989pt}{-2.39166pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\hskip 1.13809pt\scriptsize\!I}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}} and let be a mixed generator in . Then, is not a mixed generator in if and only if and for exactly one element .
Proof.
Let be a mixed generator in . Suppose that with and that . Since , it follows from the defintion of that . By transitivity, it holds that and is not a mixgen in . For the converse, by Proposition 7, we have that and, by Proposition 6 it follows that is not a mixgen in because it fails to fulfill condition of mixgens. That means that there exists with . This shows . Note that, since is the only object without the attribute in , we have that and that . From follows . Moreover, note that and, by transitivity, . We now argue that . Suppose, by contradiction, that with . Then, which implies . Therefore, which yields , contradicting the fact that is a mixed generator in . Since and , we have that . By transitivity, . ∎
Keep considering, until Proposition 14, an arbitrary context , an attribute with m^{\leavevmode\hbox to10.36pt{\vbox to10.36pt{\pgfpicture\makeatletter\hbox{\hskip 5.17923pt\lower-5.17923pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{}\pgfsys@moveto{4.97923pt}{0.0pt}\pgfsys@curveto{4.97923pt}{2.74998pt}{2.74998pt}{4.97923pt}{0.0pt}{4.97923pt}\pgfsys@curveto{-2.74998pt}{4.97923pt}{-4.97923pt}{2.74998pt}{-4.97923pt}{0.0pt}\pgfsys@curveto{-4.97923pt}{-2.74998pt}{-2.74998pt}{-4.97923pt}{0.0pt}{-4.97923pt}\pgfsys@curveto{2.74998pt}{-4.97923pt}{4.97923pt}{-2.74998pt}{4.97923pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.7989pt}{-2.39166pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\hskip 1.13809pt\scriptsize\!I}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\neq\emptyset and suppose that is a complete system of m^{\leavevmode\hbox to10.36pt{\vbox to10.36pt{\pgfpicture\makeatletter\hbox{\hskip 5.17923pt\lower-5.17923pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{}\pgfsys@moveto{4.97923pt}{0.0pt}\pgfsys@curveto{4.97923pt}{2.74998pt}{2.74998pt}{4.97923pt}{0.0pt}{4.97923pt}\pgfsys@curveto{-2.74998pt}{4.97923pt}{-4.97923pt}{2.74998pt}{-4.97923pt}{0.0pt}\pgfsys@curveto{-4.97923pt}{-2.74998pt}{-2.74998pt}{-4.97923pt}{0.0pt}{-4.97923pt}\pgfsys@curveto{2.74998pt}{-4.97923pt}{4.97923pt}{-2.74998pt}{4.97923pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.7989pt}{-2.39166pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\hskip 1.13809pt\scriptsize\!I}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}-mixed generators in . Set, for good, R=m^{\leavevmode\hbox to10.36pt{\vbox to10.36pt{\pgfpicture\makeatletter\hbox{\hskip 5.17923pt\lower-5.17923pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{}\pgfsys@moveto{4.97923pt}{0.0pt}\pgfsys@curveto{4.97923pt}{2.74998pt}{2.74998pt}{4.97923pt}{0.0pt}{4.97923pt}\pgfsys@curveto{-2.74998pt}{4.97923pt}{-4.97923pt}{2.74998pt}{-4.97923pt}{0.0pt}\pgfsys@curveto{-4.97923pt}{-2.74998pt}{-2.74998pt}{-4.97923pt}{0.0pt}{-4.97923pt}\pgfsys@curveto{2.74998pt}{-4.97923pt}{4.97923pt}{-2.74998pt}{4.97923pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.7989pt}{-2.39166pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\hskip 1.13809pt\scriptsize\!I}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}, consider a fixed object and define .
We divide in four classes:
[TABLE]
where
[TABLE]
Notice that whenever , it holds that . In contrast, a mixed generator always contains . To see this, it suffices to realize that a subset always satisfies (exactly) one of the equalities and .
Mixgens in and in are sufficiently manageable so that we may map them directly to the set of all mixed generators of and hope that they form a representative system. We will “rescue” all the mixed generators in and some in by applying the restriction mapping . Since is always a mixgen in (provided is a mixgen in ), it is easy to realize that and : indeed, in , the set is the unique mixed generator of itself (cf. Proposition 7), which forces whenever is a complete system of mixgens. Also, the equality is obvious.
The operation changes the derivation of objects in . Therefore, it makes sense to devote special attention to mixgens which have non-empty intersection with . In contrast, we need a condition which is stronger than to help us identify mixgens which are largely unaffected by the operation . Let and . We say that strongly avoids if S^{I}\cap(h^{\leavevmode\hbox to10.36pt{\vbox to10.36pt{\pgfpicture\makeatletter\hbox{\hskip 5.17923pt\lower-5.17923pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{}\pgfsys@moveto{4.97923pt}{0.0pt}\pgfsys@curveto{4.97923pt}{2.74998pt}{2.74998pt}{4.97923pt}{0.0pt}{4.97923pt}\pgfsys@curveto{-2.74998pt}{4.97923pt}{-4.97923pt}{2.74998pt}{-4.97923pt}{0.0pt}\pgfsys@curveto{-4.97923pt}{-2.74998pt}{-2.74998pt}{-4.97923pt}{0.0pt}{-4.97923pt}\pgfsys@curveto{2.74998pt}{-4.97923pt}{4.97923pt}{-2.74998pt}{4.97923pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.7989pt}{-2.39166pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\hskip 1.13809pt\scriptsize\!I}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\setminus\{m\})\neq\emptyset. That is, does not belong to and, in particular, neither to or to . Further, we define:
[TABLE]
The following claim follows directly from the antitone property of the derivation operator:
Proposition 9**.**
Let with . Then, .
We shall be able to “rescue” mixed generators in which contain each element of . Define:
[TABLE]
It turns out that the function is able to distinguish the image sets and , as the following two propositions show.
Proposition 10**.**
Let . Then, .
Proof.
Set and suppose that . Let . Note that . Because is a mixed generator and , it follows that . Therefore, there exists such that n\in h^{\leavevmode\hbox to10.36pt{\vbox to10.36pt{\pgfpicture\makeatletter\hbox{\hskip 5.17923pt\lower-5.17923pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{}\pgfsys@moveto{4.97923pt}{0.0pt}\pgfsys@curveto{4.97923pt}{2.74998pt}{2.74998pt}{4.97923pt}{0.0pt}{4.97923pt}\pgfsys@curveto{-2.74998pt}{4.97923pt}{-4.97923pt}{2.74998pt}{-4.97923pt}{0.0pt}\pgfsys@curveto{-4.97923pt}{-2.74998pt}{-2.74998pt}{-4.97923pt}{0.0pt}{-4.97923pt}\pgfsys@curveto{2.74998pt}{-4.97923pt}{4.97923pt}{-2.74998pt}{4.97923pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.7989pt}{-2.39166pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\hskip 1.13809pt\scriptsize\!I}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}} and . In particular, (S\setminus\{h\})^{I}\cap(h^{\leavevmode\hbox to10.36pt{\vbox to10.36pt{\pgfpicture\makeatletter\hbox{\hskip 5.17923pt\lower-5.17923pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{}\pgfsys@moveto{4.97923pt}{0.0pt}\pgfsys@curveto{4.97923pt}{2.74998pt}{2.74998pt}{4.97923pt}{0.0pt}{4.97923pt}\pgfsys@curveto{-2.74998pt}{4.97923pt}{-4.97923pt}{2.74998pt}{-4.97923pt}{0.0pt}\pgfsys@curveto{-4.97923pt}{-2.74998pt}{-2.74998pt}{-4.97923pt}{0.0pt}{-4.97923pt}\pgfsys@curveto{2.74998pt}{-4.97923pt}{4.97923pt}{-2.74998pt}{4.97923pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.7989pt}{-2.39166pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\hskip 1.13809pt\scriptsize\!I}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\setminus\{m\})\neq\emptyset, which is to say that the set strongly avoids . That is, , where the containment follows from Proposition 9. Since the object was arbitrary, we have that . For the remaining case, necessarily . The condition allows us to take an attribute . Clearly n\in g^{\leavevmode\hbox to10.36pt{\vbox to10.36pt{\pgfpicture\makeatletter\hbox{\hskip 5.17923pt\lower-5.17923pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{}\pgfsys@moveto{4.97923pt}{0.0pt}\pgfsys@curveto{4.97923pt}{2.74998pt}{2.74998pt}{4.97923pt}{0.0pt}{4.97923pt}\pgfsys@curveto{-2.74998pt}{4.97923pt}{-4.97923pt}{2.74998pt}{-4.97923pt}{0.0pt}\pgfsys@curveto{-4.97923pt}{-2.74998pt}{-2.74998pt}{-4.97923pt}{0.0pt}{-4.97923pt}\pgfsys@curveto{2.74998pt}{-4.97923pt}{4.97923pt}{-2.74998pt}{4.97923pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.7989pt}{-2.39166pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\hskip 1.13809pt\scriptsize\!I}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}, because is the only object whose derivation with respect to and differ. Similarly, for every because of . Note that forces which in turn implies and, as a consequence, . Combining those assertions we arrive, in particular, at (S\setminus\{g\})^{I}\cap(g^{\leavevmode\hbox to10.36pt{\vbox to10.36pt{\pgfpicture\makeatletter\hbox{\hskip 5.17923pt\lower-5.17923pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{}\pgfsys@moveto{4.97923pt}{0.0pt}\pgfsys@curveto{4.97923pt}{2.74998pt}{2.74998pt}{4.97923pt}{0.0pt}{4.97923pt}\pgfsys@curveto{-2.74998pt}{4.97923pt}{-4.97923pt}{2.74998pt}{-4.97923pt}{0.0pt}\pgfsys@curveto{-4.97923pt}{-2.74998pt}{-2.74998pt}{-4.97923pt}{0.0pt}{-4.97923pt}\pgfsys@curveto{2.74998pt}{-4.97923pt}{4.97923pt}{-2.74998pt}{4.97923pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.7989pt}{-2.39166pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\hskip 1.13809pt\scriptsize\!I}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\setminus\{m\})\neq\emptyset, that is, . ∎
Proposition 11**.**
Let . Then, .
Proof.
By Proposition 8, it follows that with and . Of course, and by transitivity, . Thus, the only attribute satisfying n\in h^{\leavevmode\hbox to10.36pt{\vbox to10.36pt{\pgfpicture\makeatletter\hbox{\hskip 5.17923pt\lower-5.17923pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{}\pgfsys@moveto{4.97923pt}{0.0pt}\pgfsys@curveto{4.97923pt}{2.74998pt}{2.74998pt}{4.97923pt}{0.0pt}{4.97923pt}\pgfsys@curveto{-2.74998pt}{4.97923pt}{-4.97923pt}{2.74998pt}{-4.97923pt}{0.0pt}\pgfsys@curveto{-4.97923pt}{-2.74998pt}{-2.74998pt}{-4.97923pt}{0.0pt}{-4.97923pt}\pgfsys@curveto{2.74998pt}{-4.97923pt}{4.97923pt}{-2.74998pt}{4.97923pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.7989pt}{-2.39166pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\hskip 1.13809pt\scriptsize\!I}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}} and is . Consequently, the intersection between h^{\leavevmode\hbox to10.36pt{\vbox to10.36pt{\pgfpicture\makeatletter\hbox{\hskip 5.17923pt\lower-5.17923pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{}\pgfsys@moveto{4.97923pt}{0.0pt}\pgfsys@curveto{4.97923pt}{2.74998pt}{2.74998pt}{4.97923pt}{0.0pt}{4.97923pt}\pgfsys@curveto{-2.74998pt}{4.97923pt}{-4.97923pt}{2.74998pt}{-4.97923pt}{0.0pt}\pgfsys@curveto{-4.97923pt}{-2.74998pt}{-2.74998pt}{-4.97923pt}{0.0pt}{-4.97923pt}\pgfsys@curveto{2.74998pt}{-4.97923pt}{4.97923pt}{-2.74998pt}{4.97923pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.7989pt}{-2.39166pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\hskip 1.13809pt\scriptsize\!I}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\setminus\{m\} and is empty, that is, the set does not strongly avoid . ∎
In order to organize to which subset of the restriction mapping maps to, we partition the class in three:
[TABLE]
Suppose that is a mixed generator in . Proposition 5 guarantees that is a mixed generator in as well. Thus, we may consider each mixed generator in pairs . Such pairs potentially collapse, i.e., it could be that and, to avoid this, we only consider a mixgen in this pairwise way when certainly does not contain already: more specifically, when . The general situation regarding the seven partition classes we defined, together with the relevant mappings is as retracted in Figure 4. An example of such a decomposition is given in Figure 5. Notice that such a partition of depends on , which in turn depends on the choice of and of g\in m^{\leavevmode\hbox to10.36pt{\vbox to10.36pt{\pgfpicture\makeatletter\hbox{\hskip 5.17923pt\lower-5.17923pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{}\pgfsys@moveto{4.97923pt}{0.0pt}\pgfsys@curveto{4.97923pt}{2.74998pt}{2.74998pt}{4.97923pt}{0.0pt}{4.97923pt}\pgfsys@curveto{-2.74998pt}{4.97923pt}{-4.97923pt}{2.74998pt}{-4.97923pt}{0.0pt}\pgfsys@curveto{-4.97923pt}{-2.74998pt}{-2.74998pt}{-4.97923pt}{0.0pt}{-4.97923pt}\pgfsys@curveto{2.74998pt}{-4.97923pt}{4.97923pt}{-2.74998pt}{4.97923pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.7989pt}{-2.39166pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\hskip 1.13809pt\scriptsize\!I}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}.
The reader has probably noticed from the characterization of elements in that the derivation is not much different from whenever . Indeed, they differ only by the presence of the attribute . As a result, the restriction mapping is injective when applied to that class:
Proposition 12**.**
The restriction mapping is injective when applied to .
Proof.
Let and suppose that . By Proposition 8, one has that and, in particular, . Moreover, Proposition 8 implies as well as . From follows and yields . Since is a representative system of mixgens, this forces . ∎
Consider the context depicted earlier in Figures 1 and 2. Further, consider the complete system of mixed generators given in (1). Figure 5 illustrates the partition described in Figure 4 with . Note that, in , and, therefore, when keeping fixed, we have two (potentially different) decompositions: one for each choice of . To ease the notation we shall, from now on, omit the superscript and write only and whenever we partition in three (that is, ).
Regarding the same complete system of mixgens but with a different choice of , namely , we have the decomposition depicted in Figure 6.
Before we consider the images of the mappings present in Figure 4 and establish whether they form a representative system in or not, we shall turn our attention for a moment to the closure operator in . More specifically, we shall relate it to the closure operator in and to the function . For that, we define
[TABLE]
The functions (and therefore ) are to be calculated always regarding the original incidence relation, that is, .
Proposition 13**.**
Let . Then:
[TABLE]
Furthermore, and .
Proof.
Whenever , the set is a mixgen in and such that , and Proposition 2 assures that is an extent in both contexts. If then, clearly, as well as . Now, suppose that . Proposition 8 implies that we have in case that . The same equality follows easily from the definition of , so that that relationship is valid in either case. Then, it follows that .
Regarding the last two assertions, we assume since otherwise both follow trivially from the already established fact that is an extent in both contexts. For the second claim: take an object . Since is a mixed generator in , we have that and it is clear that h^{\leavevmode\hbox to10.36pt{\vbox to10.36pt{\pgfpicture\makeatletter\hbox{\hskip 5.17923pt\lower-5.17923pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{}\pgfsys@moveto{4.97923pt}{0.0pt}\pgfsys@curveto{4.97923pt}{2.74998pt}{2.74998pt}{4.97923pt}{0.0pt}{4.97923pt}\pgfsys@curveto{-2.74998pt}{4.97923pt}{-4.97923pt}{2.74998pt}{-4.97923pt}{0.0pt}\pgfsys@curveto{-4.97923pt}{-2.74998pt}{-2.74998pt}{-4.97923pt}{0.0pt}{-4.97923pt}\pgfsys@curveto{2.74998pt}{-4.97923pt}{4.97923pt}{-2.74998pt}{4.97923pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.7989pt}{-2.39166pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\hskip 1.13809pt\scriptsize\!I}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\cap S^{I}=\emptyset and, consequently, does not strongly avoid . Now, let . We may suppose : indeed, in , the object is an extremal point of every extent containing it, that is, implies . Of course, is equivalent to the condition of h^{\leavevmode\hbox to10.36pt{\vbox to10.36pt{\pgfpicture\makeatletter\hbox{\hskip 5.17923pt\lower-5.17923pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{}\pgfsys@moveto{4.97923pt}{0.0pt}\pgfsys@curveto{4.97923pt}{2.74998pt}{2.74998pt}{4.97923pt}{0.0pt}{4.97923pt}\pgfsys@curveto{-2.74998pt}{4.97923pt}{-4.97923pt}{2.74998pt}{-4.97923pt}{0.0pt}\pgfsys@curveto{-4.97923pt}{-2.74998pt}{-2.74998pt}{-4.97923pt}{0.0pt}{-4.97923pt}\pgfsys@curveto{2.74998pt}{-4.97923pt}{4.97923pt}{-2.74998pt}{4.97923pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.7989pt}{-2.39166pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\hskip 1.13809pt\scriptsize\!I}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\cap S^{I} being non-empty, whereas if and only if h^{\leavevmode\hbox to10.36pt{\vbox to10.36pt{\pgfpicture\makeatletter\hbox{\hskip 5.17923pt\lower-5.17923pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{}\pgfsys@moveto{4.97923pt}{0.0pt}\pgfsys@curveto{4.97923pt}{2.74998pt}{2.74998pt}{4.97923pt}{0.0pt}{4.97923pt}\pgfsys@curveto{-2.74998pt}{4.97923pt}{-4.97923pt}{2.74998pt}{-4.97923pt}{0.0pt}\pgfsys@curveto{-4.97923pt}{-2.74998pt}{-2.74998pt}{-4.97923pt}{0.0pt}{-4.97923pt}\pgfsys@curveto{2.74998pt}{-4.97923pt}{4.97923pt}{-2.74998pt}{4.97923pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.26314pt}{-2.39166pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\hskip 1.13809pt\scriptsize\!J}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}} and are disjoint. Since and h^{\leavevmode\hbox to10.36pt{\vbox to10.36pt{\pgfpicture\makeatletter\hbox{\hskip 5.17923pt\lower-5.17923pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{}\pgfsys@moveto{4.97923pt}{0.0pt}\pgfsys@curveto{4.97923pt}{2.74998pt}{2.74998pt}{4.97923pt}{0.0pt}{4.97923pt}\pgfsys@curveto{-2.74998pt}{4.97923pt}{-4.97923pt}{2.74998pt}{-4.97923pt}{0.0pt}\pgfsys@curveto{-4.97923pt}{-2.74998pt}{-2.74998pt}{-4.97923pt}{0.0pt}{-4.97923pt}\pgfsys@curveto{2.74998pt}{-4.97923pt}{4.97923pt}{-2.74998pt}{4.97923pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.26314pt}{-2.39166pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\hskip 1.13809pt\scriptsize\!J}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}=h^{\leavevmode\hbox to10.36pt{\vbox to10.36pt{\pgfpicture\makeatletter\hbox{\hskip 5.17923pt\lower-5.17923pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{}\pgfsys@moveto{4.97923pt}{0.0pt}\pgfsys@curveto{4.97923pt}{2.74998pt}{2.74998pt}{4.97923pt}{0.0pt}{4.97923pt}\pgfsys@curveto{-2.74998pt}{4.97923pt}{-4.97923pt}{2.74998pt}{-4.97923pt}{0.0pt}\pgfsys@curveto{-4.97923pt}{-2.74998pt}{-2.74998pt}{-4.97923pt}{0.0pt}{-4.97923pt}\pgfsys@curveto{2.74998pt}{-4.97923pt}{4.97923pt}{-2.74998pt}{4.97923pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.7989pt}{-2.39166pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\hskip 1.13809pt\scriptsize\!I}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}} or h^{\leavevmode\hbox to10.36pt{\vbox to10.36pt{\pgfpicture\makeatletter\hbox{\hskip 5.17923pt\lower-5.17923pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{}\pgfsys@moveto{4.97923pt}{0.0pt}\pgfsys@curveto{4.97923pt}{2.74998pt}{2.74998pt}{4.97923pt}{0.0pt}{4.97923pt}\pgfsys@curveto{-2.74998pt}{4.97923pt}{-4.97923pt}{2.74998pt}{-4.97923pt}{0.0pt}\pgfsys@curveto{-4.97923pt}{-2.74998pt}{-2.74998pt}{-4.97923pt}{0.0pt}{-4.97923pt}\pgfsys@curveto{2.74998pt}{-4.97923pt}{4.97923pt}{-2.74998pt}{4.97923pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.26314pt}{-2.39166pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\hskip 1.13809pt\scriptsize\!J}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}=h^{\leavevmode\hbox to10.36pt{\vbox to10.36pt{\pgfpicture\makeatletter\hbox{\hskip 5.17923pt\lower-5.17923pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{}\pgfsys@moveto{4.97923pt}{0.0pt}\pgfsys@curveto{4.97923pt}{2.74998pt}{2.74998pt}{4.97923pt}{0.0pt}{4.97923pt}\pgfsys@curveto{-2.74998pt}{4.97923pt}{-4.97923pt}{2.74998pt}{-4.97923pt}{0.0pt}\pgfsys@curveto{-4.97923pt}{-2.74998pt}{-2.74998pt}{-4.97923pt}{0.0pt}{-4.97923pt}\pgfsys@curveto{2.74998pt}{-4.97923pt}{4.97923pt}{-2.74998pt}{4.97923pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.7989pt}{-2.39166pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\hskip 1.13809pt\scriptsize\!I}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\setminus\{m\}, only the second equality may and must hold, which implies , as well as h^{\leavevmode\hbox to10.36pt{\vbox to10.36pt{\pgfpicture\makeatletter\hbox{\hskip 5.17923pt\lower-5.17923pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{}\pgfsys@moveto{4.97923pt}{0.0pt}\pgfsys@curveto{4.97923pt}{2.74998pt}{2.74998pt}{4.97923pt}{0.0pt}{4.97923pt}\pgfsys@curveto{-2.74998pt}{4.97923pt}{-4.97923pt}{2.74998pt}{-4.97923pt}{0.0pt}\pgfsys@curveto{-4.97923pt}{-2.74998pt}{-2.74998pt}{-4.97923pt}{0.0pt}{-4.97923pt}\pgfsys@curveto{2.74998pt}{-4.97923pt}{4.97923pt}{-2.74998pt}{4.97923pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.7989pt}{-2.39166pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\hskip 1.13809pt\scriptsize\!I}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\cap S^{I}=\{m\}. In particular, the set does not strongly avoid . ∎
The following theorem gives information about derivation in of mixed generators which were mapped from and shows a sufficient condition for .
Theorem 3**.**
The mappings and are injections, respectively, from and into the set of all mixed generators of . Their images are disjoint sets whose union is a representative system. The corresponding intents are given by
[TABLE]
where denotes domain restriction. Intents which already were intents of the original context are characterized via and . The corresponding extents are given by
[TABLE]
In particular, whenever is finite.
Proof.
The set is always a mixed generator because of Proposition 5. We show the formulas for the intents. Let . Then, . Suppose that . Then, . Now, let . Consequently, one has , and . The first two facts together with imply . Lastly, . Before proving the properties of the mappings, we prove the two equivalences mentioned.
Let . We prove that is not an intent of . Note that . Suppose, by contradiction, that there exists with . In particular, , which implies for each . Since , it follows that and this, combined with the fact that is a mixed generator, yields . Moreover, one has of course that and, on the other hand and imply . We arrive at , which contradicts the fact that is a mixed generator in . Now, let . We show that is not an intent of . Set . Since , it follows that the set (S^{I}\setminus\{m\})\cap h^{\leavevmode\hbox to10.36pt{\vbox to10.36pt{\pgfpicture\makeatletter\hbox{\hskip 5.17923pt\lower-5.17923pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{}\pgfsys@moveto{4.97923pt}{0.0pt}\pgfsys@curveto{4.97923pt}{2.74998pt}{2.74998pt}{4.97923pt}{0.0pt}{4.97923pt}\pgfsys@curveto{-2.74998pt}{4.97923pt}{-4.97923pt}{2.74998pt}{-4.97923pt}{0.0pt}\pgfsys@curveto{-4.97923pt}{-2.74998pt}{-2.74998pt}{-4.97923pt}{0.0pt}{-4.97923pt}\pgfsys@curveto{2.74998pt}{-4.97923pt}{4.97923pt}{-2.74998pt}{4.97923pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.7989pt}{-2.39166pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\hskip 1.13809pt\scriptsize\!I}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}=B\cap h^{\leavevmode\hbox to10.36pt{\vbox to10.36pt{\pgfpicture\makeatletter\hbox{\hskip 5.17923pt\lower-5.17923pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{}\pgfsys@moveto{4.97923pt}{0.0pt}\pgfsys@curveto{4.97923pt}{2.74998pt}{2.74998pt}{4.97923pt}{0.0pt}{4.97923pt}\pgfsys@curveto{-2.74998pt}{4.97923pt}{-4.97923pt}{2.74998pt}{-4.97923pt}{0.0pt}\pgfsys@curveto{-4.97923pt}{-2.74998pt}{-2.74998pt}{-4.97923pt}{0.0pt}{-4.97923pt}\pgfsys@curveto{2.74998pt}{-4.97923pt}{4.97923pt}{-2.74998pt}{4.97923pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.7989pt}{-2.39166pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\hskip 1.13809pt\scriptsize\!I}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}} is non-empty for each . Now, for any set , an equality requires that , which clearly forces T^{I}\cap h^{\leavevmode\hbox to10.36pt{\vbox to10.36pt{\pgfpicture\makeatletter\hbox{\hskip 5.17923pt\lower-5.17923pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{}\pgfsys@moveto{4.97923pt}{0.0pt}\pgfsys@curveto{4.97923pt}{2.74998pt}{2.74998pt}{4.97923pt}{0.0pt}{4.97923pt}\pgfsys@curveto{-2.74998pt}{4.97923pt}{-4.97923pt}{2.74998pt}{-4.97923pt}{0.0pt}\pgfsys@curveto{-4.97923pt}{-2.74998pt}{-2.74998pt}{-4.97923pt}{0.0pt}{-4.97923pt}\pgfsys@curveto{2.74998pt}{-4.97923pt}{4.97923pt}{-2.74998pt}{4.97923pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.7989pt}{-2.39166pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\hskip 1.13809pt\scriptsize\!I}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}=\emptyset for some and, therefore, in any case, it holds that .
Note that in case that and, similarly, whenever . Combining this with the shown formulas for the intents, as well as with the fact that the sets are drawn from a representative system, it follows that each of the restricted, composite mappings maps into the set of intents of . We will now show that those four mappings have disjoint image sets. Let . Since is an intent of whereas is not, it follows, in particular, that . Moreover we have, as shown, and . An equality can not hold since this would force , which is not possible in a representative system. Now, let and . The intent formula implies that is an intent of , whereas is not. Thus, . Lastly, it is trivial that and , causing . Regarding the extents, we first prove that . Indeed, for an object one has that does not strongly avoid , that is, h^{\leavevmode\hbox to10.36pt{\vbox to10.36pt{\pgfpicture\makeatletter\hbox{\hskip 5.17923pt\lower-5.17923pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{}\pgfsys@moveto{4.97923pt}{0.0pt}\pgfsys@curveto{4.97923pt}{2.74998pt}{2.74998pt}{4.97923pt}{0.0pt}{4.97923pt}\pgfsys@curveto{-2.74998pt}{4.97923pt}{-4.97923pt}{2.74998pt}{-4.97923pt}{0.0pt}\pgfsys@curveto{-4.97923pt}{-2.74998pt}{-2.74998pt}{-4.97923pt}{0.0pt}{-4.97923pt}\pgfsys@curveto{2.74998pt}{-4.97923pt}{4.97923pt}{-2.74998pt}{4.97923pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.7989pt}{-2.39166pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\hskip 1.13809pt\scriptsize\!I}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\cap S^{I}\subseteq\{m\}. Now, since is distinct from , it follows that h^{\leavevmode\hbox to10.36pt{\vbox to10.36pt{\pgfpicture\makeatletter\hbox{\hskip 5.17923pt\lower-5.17923pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{}\pgfsys@moveto{4.97923pt}{0.0pt}\pgfsys@curveto{4.97923pt}{2.74998pt}{2.74998pt}{4.97923pt}{0.0pt}{4.97923pt}\pgfsys@curveto{-2.74998pt}{4.97923pt}{-4.97923pt}{2.74998pt}{-4.97923pt}{0.0pt}\pgfsys@curveto{-4.97923pt}{-2.74998pt}{-2.74998pt}{-4.97923pt}{0.0pt}{-4.97923pt}\pgfsys@curveto{2.74998pt}{-4.97923pt}{4.97923pt}{-2.74998pt}{4.97923pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.26314pt}{-2.39166pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\hskip 1.13809pt\scriptsize\!J}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}=h^{\leavevmode\hbox to10.36pt{\vbox to10.36pt{\pgfpicture\makeatletter\hbox{\hskip 5.17923pt\lower-5.17923pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{}\pgfsys@moveto{4.97923pt}{0.0pt}\pgfsys@curveto{4.97923pt}{2.74998pt}{2.74998pt}{4.97923pt}{0.0pt}{4.97923pt}\pgfsys@curveto{-2.74998pt}{4.97923pt}{-4.97923pt}{2.74998pt}{-4.97923pt}{0.0pt}\pgfsys@curveto{-4.97923pt}{-2.74998pt}{-2.74998pt}{-4.97923pt}{0.0pt}{-4.97923pt}\pgfsys@curveto{2.74998pt}{-4.97923pt}{4.97923pt}{-2.74998pt}{4.97923pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.7989pt}{-2.39166pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\hskip 1.13809pt\scriptsize\!I}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\setminus\{m\}. Consequently, \emptyset=h^{\leavevmode\hbox to10.36pt{\vbox to10.36pt{\pgfpicture\makeatletter\hbox{\hskip 5.17923pt\lower-5.17923pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{}\pgfsys@moveto{4.97923pt}{0.0pt}\pgfsys@curveto{4.97923pt}{2.74998pt}{2.74998pt}{4.97923pt}{0.0pt}{4.97923pt}\pgfsys@curveto{-2.74998pt}{4.97923pt}{-4.97923pt}{2.74998pt}{-4.97923pt}{0.0pt}\pgfsys@curveto{-4.97923pt}{-2.74998pt}{-2.74998pt}{-4.97923pt}{0.0pt}{-4.97923pt}\pgfsys@curveto{2.74998pt}{-4.97923pt}{4.97923pt}{-2.74998pt}{4.97923pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.26314pt}{-2.39166pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\hskip 1.13809pt\scriptsize\!J}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\cap S^{I} and, in any case, the calculated intent is a subset of , which causes h^{\leavevmode\hbox to10.36pt{\vbox to10.36pt{\pgfpicture\makeatletter\hbox{\hskip 5.17923pt\lower-5.17923pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{}\pgfsys@moveto{4.97923pt}{0.0pt}\pgfsys@curveto{4.97923pt}{2.74998pt}{2.74998pt}{4.97923pt}{0.0pt}{4.97923pt}\pgfsys@curveto{-2.74998pt}{4.97923pt}{-4.97923pt}{2.74998pt}{-4.97923pt}{0.0pt}\pgfsys@curveto{-4.97923pt}{-2.74998pt}{-2.74998pt}{-4.97923pt}{0.0pt}{-4.97923pt}\pgfsys@curveto{2.74998pt}{-4.97923pt}{4.97923pt}{-2.74998pt}{4.97923pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.26314pt}{-2.39166pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\hskip 1.13809pt\scriptsize\!J}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\cap S^{J}=\emptyset, that is, . Combining this fact with the following two properties yields the formula for : first, for each , one has that implies , and the converse is obvious. Second, Proposition 13 guarantees that, in general (except when ), as well as and . The formula for follows from the one for and from the fact that is an extremal point of every extent containing . ∎
We now investigate what happens to the seven classes depicted in Figure 4 when one changes the object g\in m^{\leavevmode\hbox to10.36pt{\vbox to10.36pt{\pgfpicture\makeatletter\hbox{\hskip 5.17923pt\lower-5.17923pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{}\pgfsys@moveto{4.97923pt}{0.0pt}\pgfsys@curveto{4.97923pt}{2.74998pt}{2.74998pt}{4.97923pt}{0.0pt}{4.97923pt}\pgfsys@curveto{-2.74998pt}{4.97923pt}{-4.97923pt}{2.74998pt}{-4.97923pt}{0.0pt}\pgfsys@curveto{-4.97923pt}{-2.74998pt}{-2.74998pt}{-4.97923pt}{0.0pt}{-4.97923pt}\pgfsys@curveto{2.74998pt}{-4.97923pt}{4.97923pt}{-2.74998pt}{4.97923pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.7989pt}{-2.39166pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\hskip 1.13809pt\scriptsize\!I}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}} chosen to perform the operation . The attribute , however, is to be considered fixed. Note that, for a fixed set , the function value depends on but does not depend on .
Lemma 1** (stability).**
The classes and do not depend on the choice of . Moreover, let . Then,
[TABLE]
In particular, does not depend on the choice of .
Proof.
The claim regarding is clear because implies , which means that is always , independently of the choice of . Likewise, the value of the function does not depend on either. We now assume |m^{\leavevmode\hbox to10.36pt{\vbox to10.36pt{\pgfpicture\makeatletter\hbox{\hskip 5.17923pt\lower-5.17923pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{}\pgfsys@moveto{4.97923pt}{0.0pt}\pgfsys@curveto{4.97923pt}{2.74998pt}{2.74998pt}{4.97923pt}{0.0pt}{4.97923pt}\pgfsys@curveto{-2.74998pt}{4.97923pt}{-4.97923pt}{2.74998pt}{-4.97923pt}{0.0pt}\pgfsys@curveto{-4.97923pt}{-2.74998pt}{-2.74998pt}{-4.97923pt}{0.0pt}{-4.97923pt}\pgfsys@curveto{2.74998pt}{-4.97923pt}{4.97923pt}{-2.74998pt}{4.97923pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.7989pt}{-2.39166pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\hskip 1.13809pt\scriptsize\!I}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}|\geq 2. Let for some choice of . Let h\in m^{\leavevmode\hbox to10.36pt{\vbox to10.36pt{\pgfpicture\makeatletter\hbox{\hskip 5.17923pt\lower-5.17923pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{}\pgfsys@moveto{4.97923pt}{0.0pt}\pgfsys@curveto{4.97923pt}{2.74998pt}{2.74998pt}{4.97923pt}{0.0pt}{4.97923pt}\pgfsys@curveto{-2.74998pt}{4.97923pt}{-4.97923pt}{2.74998pt}{-4.97923pt}{0.0pt}\pgfsys@curveto{-4.97923pt}{-2.74998pt}{-2.74998pt}{-4.97923pt}{0.0pt}{-4.97923pt}\pgfsys@curveto{2.74998pt}{-4.97923pt}{4.97923pt}{-2.74998pt}{4.97923pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.7989pt}{-2.39166pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\hskip 1.13809pt\scriptsize\!I}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}} with and denote by the incidence relation of . The fact that is a mixgen causes , which means that there exists n\in h^{\leavevmode\hbox to10.36pt{\vbox to10.36pt{\pgfpicture\makeatletter\hbox{\hskip 5.17923pt\lower-5.17923pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{}\pgfsys@moveto{4.97923pt}{0.0pt}\pgfsys@curveto{4.97923pt}{2.74998pt}{2.74998pt}{4.97923pt}{0.0pt}{4.97923pt}\pgfsys@curveto{-2.74998pt}{4.97923pt}{-4.97923pt}{2.74998pt}{-4.97923pt}{0.0pt}\pgfsys@curveto{-4.97923pt}{-2.74998pt}{-2.74998pt}{-4.97923pt}{0.0pt}{-4.97923pt}\pgfsys@curveto{2.74998pt}{-4.97923pt}{4.97923pt}{-2.74998pt}{4.97923pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.7989pt}{-2.39166pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\hskip 1.13809pt\scriptsize\!I}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}} with . Note that . Since , and g\in m^{\leavevmode\hbox to10.36pt{\vbox to10.36pt{\pgfpicture\makeatletter\hbox{\hskip 5.17923pt\lower-5.17923pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{}\pgfsys@moveto{4.97923pt}{0.0pt}\pgfsys@curveto{4.97923pt}{2.74998pt}{2.74998pt}{4.97923pt}{0.0pt}{4.97923pt}\pgfsys@curveto{-2.74998pt}{4.97923pt}{-4.97923pt}{2.74998pt}{-4.97923pt}{0.0pt}\pgfsys@curveto{-4.97923pt}{-2.74998pt}{-2.74998pt}{-4.97923pt}{0.0pt}{-4.97923pt}\pgfsys@curveto{2.74998pt}{-4.97923pt}{4.97923pt}{-2.74998pt}{4.97923pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.7989pt}{-2.39166pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\hskip 1.13809pt\scriptsize\!I}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}, we have and . Hence, in particular, and , which causes for the choice .
For the first equivalence, let and . We need to show first that . If , then both containments follow from Proposition 8. If not, then and . We assume because, otherwise, forces and then there is nothing to prove. First we prove that does not strongly avoid . Set . A simple calculation shows and, consequently, , that is, (S\setminus\{g\})^{I}\cap g^{\leavevmode\hbox to10.36pt{\vbox to10.36pt{\pgfpicture\makeatletter\hbox{\hskip 5.17923pt\lower-5.17923pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{}\pgfsys@moveto{4.97923pt}{0.0pt}\pgfsys@curveto{4.97923pt}{2.74998pt}{2.74998pt}{4.97923pt}{0.0pt}{4.97923pt}\pgfsys@curveto{-2.74998pt}{4.97923pt}{-4.97923pt}{2.74998pt}{-4.97923pt}{0.0pt}\pgfsys@curveto{-4.97923pt}{-2.74998pt}{-2.74998pt}{-4.97923pt}{0.0pt}{-4.97923pt}\pgfsys@curveto{2.74998pt}{-4.97923pt}{4.97923pt}{-2.74998pt}{4.97923pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.7989pt}{-2.39166pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\hskip 1.13809pt\scriptsize\!I}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\subseteq\{m\} and does not strongly avoid . It must hold as well that because, otherwise, we would have and , contradicting that is a mixgen. In any case, the containments hold and, consequently, for arbitrary :
[TABLE]
For the converse, suppose that , that is, . Set . Clearly, . Suppose that and take . Then, since is a mixgen, it follows that , which is equivalent to (S\setminus\{h\})^{I}\cap h^{\leavevmode\hbox to10.36pt{\vbox to10.36pt{\pgfpicture\makeatletter\hbox{\hskip 5.17923pt\lower-5.17923pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{}\pgfsys@moveto{4.97923pt}{0.0pt}\pgfsys@curveto{4.97923pt}{2.74998pt}{2.74998pt}{4.97923pt}{0.0pt}{4.97923pt}\pgfsys@curveto{-2.74998pt}{4.97923pt}{-4.97923pt}{2.74998pt}{-4.97923pt}{0.0pt}\pgfsys@curveto{-4.97923pt}{-2.74998pt}{-2.74998pt}{-4.97923pt}{0.0pt}{-4.97923pt}\pgfsys@curveto{2.74998pt}{-4.97923pt}{4.97923pt}{-2.74998pt}{4.97923pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.7989pt}{-2.39166pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\hskip 1.13809pt\scriptsize\!I}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\neq\emptyset. From follows that , which in turn implies that strongly avoids . Proposition 9 implies that strongly avoids as well and, consequently, . For the case , suppose additionally that . Then, with , since no element in may contain . We claim that contains properly . The containment is clear, we have to discard equality: if then, and, by Proposition 8, the set would belong to (and not to ). Therefore, there exists with n\neq m,n\in h^{\leavevmode\hbox to10.36pt{\vbox to10.36pt{\pgfpicture\makeatletter\hbox{\hskip 5.17923pt\lower-5.17923pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{}\pgfsys@moveto{4.97923pt}{0.0pt}\pgfsys@curveto{4.97923pt}{2.74998pt}{2.74998pt}{4.97923pt}{0.0pt}{4.97923pt}\pgfsys@curveto{-2.74998pt}{4.97923pt}{-4.97923pt}{2.74998pt}{-4.97923pt}{0.0pt}\pgfsys@curveto{-4.97923pt}{-2.74998pt}{-2.74998pt}{-4.97923pt}{0.0pt}{-4.97923pt}\pgfsys@curveto{2.74998pt}{-4.97923pt}{4.97923pt}{-2.74998pt}{4.97923pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.7989pt}{-2.39166pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\hskip 1.13809pt\scriptsize\!I}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}. Consequently, strongly avoids and, like before, . Now, suppose that . In this case, . Take an element with . Since the only object with is , it holds that and n\in g^{\leavevmode\hbox to10.36pt{\vbox to10.36pt{\pgfpicture\makeatletter\hbox{\hskip 5.17923pt\lower-5.17923pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{}\pgfsys@moveto{4.97923pt}{0.0pt}\pgfsys@curveto{4.97923pt}{2.74998pt}{2.74998pt}{4.97923pt}{0.0pt}{4.97923pt}\pgfsys@curveto{-2.74998pt}{4.97923pt}{-4.97923pt}{2.74998pt}{-4.97923pt}{0.0pt}\pgfsys@curveto{-4.97923pt}{-2.74998pt}{-2.74998pt}{-4.97923pt}{0.0pt}{-4.97923pt}\pgfsys@curveto{2.74998pt}{-4.97923pt}{4.97923pt}{-2.74998pt}{4.97923pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.7989pt}{-2.39166pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\hskip 1.13809pt\scriptsize\!I}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}. Hence, in particular, the set (S\setminus\{g\})^{I}\cap(g^{\leavevmode\hbox to10.36pt{\vbox to10.36pt{\pgfpicture\makeatletter\hbox{\hskip 5.17923pt\lower-5.17923pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{}\pgfsys@moveto{4.97923pt}{0.0pt}\pgfsys@curveto{4.97923pt}{2.74998pt}{2.74998pt}{4.97923pt}{0.0pt}{4.97923pt}\pgfsys@curveto{-2.74998pt}{4.97923pt}{-4.97923pt}{2.74998pt}{-4.97923pt}{0.0pt}\pgfsys@curveto{-4.97923pt}{-2.74998pt}{-2.74998pt}{-4.97923pt}{0.0pt}{-4.97923pt}\pgfsys@curveto{2.74998pt}{-4.97923pt}{4.97923pt}{-2.74998pt}{4.97923pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.7989pt}{-2.39166pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\hskip 1.13809pt\scriptsize\!I}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\setminus\{m\}) is non-empty, meaning that strongly avoids . The second equivalence follows from the first and Proposition 9. ∎
Instead of mapping and “internally” into , it is possible to map both directly into the set of intents of via , where denotes derivation in and adds the object , that is, is as defined in Theorem 3. The characterization of sets which are mixed generators in but not in implies that whenever . Similarly, it is clear that for every . In this setting, it is not required anymore that be complete. Moreover, we partition in two, instead of three: we set . Figure 7 illustrates those facts as well as properties stated in Theorem 3 and Lemma 1.
We say that a family of -mixed generators has the semi-downset property if the implication holds.
Proposition 14**.**
For any context with finite object set and an arbitrary there exists a complete system of -mixed generators which has the semi-downset property.
Proof.
We prove this constructively. Define some arbitrary total order on . Consider the induced lexicographic order over and for every extent , define and . We show that, for every and every , the set belongs as well to . Set . By Proposition 7, we have that is a mixed generator. Suppose, by contradiction, that . Then, there exists a set with , and as well as . Note that and imply . Then, which yields . Since is finite, we may take a mixed generator of which is a subset of (possibly itself). This contradicts . ∎
It turns out that for every there exists g\in m^{\leavevmode\hbox to10.36pt{\vbox to10.36pt{\pgfpicture\makeatletter\hbox{\hskip 5.17923pt\lower-5.17923pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{}\pgfsys@moveto{4.97923pt}{0.0pt}\pgfsys@curveto{4.97923pt}{2.74998pt}{2.74998pt}{4.97923pt}{0.0pt}{4.97923pt}\pgfsys@curveto{-2.74998pt}{4.97923pt}{-4.97923pt}{2.74998pt}{-4.97923pt}{0.0pt}\pgfsys@curveto{-4.97923pt}{-2.74998pt}{-2.74998pt}{-4.97923pt}{0.0pt}{-4.97923pt}\pgfsys@curveto{2.74998pt}{-4.97923pt}{4.97923pt}{-2.74998pt}{4.97923pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.7989pt}{-2.39166pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\hskip 1.13809pt\scriptsize\!I}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}} such that , unless the attribute corresponds to a full column in the formal context.
Theorem 4**.**
Let be a context with finite and let . Suppose that is a representative system of m^{\leavevmode\hbox to10.36pt{\vbox to10.36pt{\pgfpicture\makeatletter\hbox{\hskip 5.17923pt\lower-5.17923pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{}\pgfsys@moveto{4.97923pt}{0.0pt}\pgfsys@curveto{4.97923pt}{2.74998pt}{2.74998pt}{4.97923pt}{0.0pt}{4.97923pt}\pgfsys@curveto{-2.74998pt}{4.97923pt}{-4.97923pt}{2.74998pt}{-4.97923pt}{0.0pt}\pgfsys@curveto{-4.97923pt}{-2.74998pt}{-2.74998pt}{-4.97923pt}{0.0pt}{-4.97923pt}\pgfsys@curveto{2.74998pt}{-4.97923pt}{4.97923pt}{-2.74998pt}{4.97923pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.7989pt}{-2.39166pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\hskip 1.13809pt\scriptsize\!I}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}-mixed generators which has the semi-downset property. If does not correspond to a full column, then there exists an object g\in m^{\leavevmode\hbox to10.36pt{\vbox to10.36pt{\pgfpicture\makeatletter\hbox{\hskip 5.17923pt\lower-5.17923pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{}\pgfsys@moveto{4.97923pt}{0.0pt}\pgfsys@curveto{4.97923pt}{2.74998pt}{2.74998pt}{4.97923pt}{0.0pt}{4.97923pt}\pgfsys@curveto{-2.74998pt}{4.97923pt}{-4.97923pt}{2.74998pt}{-4.97923pt}{0.0pt}\pgfsys@curveto{-4.97923pt}{-2.74998pt}{-2.74998pt}{-4.97923pt}{0.0pt}{-4.97923pt}\pgfsys@curveto{2.74998pt}{-4.97923pt}{4.97923pt}{-2.74998pt}{4.97923pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.7989pt}{-2.39166pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\hskip 1.13809pt\scriptsize\!I}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}} such that .
Proof.
Set R=m^{\leavevmode\hbox to10.36pt{\vbox to10.36pt{\pgfpicture\makeatletter\hbox{\hskip 5.17923pt\lower-5.17923pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{}\pgfsys@moveto{4.97923pt}{0.0pt}\pgfsys@curveto{4.97923pt}{2.74998pt}{2.74998pt}{4.97923pt}{0.0pt}{4.97923pt}\pgfsys@curveto{-2.74998pt}{4.97923pt}{-4.97923pt}{2.74998pt}{-4.97923pt}{0.0pt}\pgfsys@curveto{-4.97923pt}{-2.74998pt}{-2.74998pt}{-4.97923pt}{0.0pt}{-4.97923pt}\pgfsys@curveto{2.74998pt}{-4.97923pt}{4.97923pt}{-2.74998pt}{4.97923pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.7989pt}{-2.39166pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\hskip 1.13809pt\scriptsize\!I}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}} and . We may of course suppose : otherwise and there is nothing to prove. Define for each . Notice that . For we further define
[TABLE]
Since and no set in contains whereas every set in does, it actually holds that and . Suppose, by contradiction, that for every .
[TABLE]
Summing for all :
[TABLE]
Consider a proper subset of and set . For each element of , there exists a summand on the left hand side of the inequality above ( summands). On the other hand, for each element of , there exists a summand on the right-hand side ( summands). We calculate a balance: if , the summand contributes exactly times to the left-hand side. If , the summand will appear exactly times on the right-hand side. We have, therefore
[TABLE]
(the equality above is indeed valid: for odd , it is very clear. For even , notice that equals zero for ).
On the other hand, consider the -element subsets of for each , . The semi-downset property of assures the existence of an injection from into whenever , given by the restriction . Now, for each with , take a bijection such that for every (such bijections exist by an elementary application of Hall’s theorem). Now, let , so that . Then:
[TABLE]
which contradicts (2). ∎
As a consequence, the initially posed question gets answered in the affirmative:
Corollary 1**.**
Let be a context with finite and let be an attribute which does not correspond to a full column. Then, there exists an object g\in m^{\leavevmode\hbox to10.36pt{\vbox to10.36pt{\pgfpicture\makeatletter\hbox{\hskip 5.17923pt\lower-5.17923pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{}\pgfsys@moveto{4.97923pt}{0.0pt}\pgfsys@curveto{4.97923pt}{2.74998pt}{2.74998pt}{4.97923pt}{0.0pt}{4.97923pt}\pgfsys@curveto{-2.74998pt}{4.97923pt}{-4.97923pt}{2.74998pt}{-4.97923pt}{0.0pt}\pgfsys@curveto{-4.97923pt}{-2.74998pt}{-2.74998pt}{-4.97923pt}{0.0pt}{-4.97923pt}\pgfsys@curveto{2.74998pt}{-4.97923pt}{4.97923pt}{-2.74998pt}{4.97923pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.7989pt}{-2.39166pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\hskip 1.13809pt\scriptsize\!I}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}} such that , where .
Proof.
One takes a complete system of m^{\leavevmode\hbox to10.36pt{\vbox to10.36pt{\pgfpicture\makeatletter\hbox{\hskip 5.17923pt\lower-5.17923pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{}\pgfsys@moveto{4.97923pt}{0.0pt}\pgfsys@curveto{4.97923pt}{2.74998pt}{2.74998pt}{4.97923pt}{0.0pt}{4.97923pt}\pgfsys@curveto{-2.74998pt}{4.97923pt}{-4.97923pt}{2.74998pt}{-4.97923pt}{0.0pt}\pgfsys@curveto{-4.97923pt}{-2.74998pt}{-2.74998pt}{-4.97923pt}{0.0pt}{-4.97923pt}\pgfsys@curveto{2.74998pt}{-4.97923pt}{4.97923pt}{-2.74998pt}{4.97923pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.7989pt}{-2.39166pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\hskip 1.13809pt\scriptsize\!I}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}-mixgens with the semi-downset property provided by Proposition 14 and applies Theorem 4 in order to fulfill the sufficient condition guaranteed by Theorem 3. ∎
4 Application
Let . The contranominal scale of size will be denoted . We define as the set of all formal contexts having exactly objects, attributes and having no contranominal scale of size as a subcontext. We define to be the contrast of , that is, the size of the largest contranominal scale (number of objects) that can be found as subcontext of . We say that is a contranominal-summand of if . The largest natural number (possibly zero) such that is a contranominal-summand of will be denoted by . Obviously, is a lower bound of . The noncontranominal kernel of is if with . It is unique222The noncontranominal kernel corresponds to the connected components of the hypergraph \{h^{\leavevmode\hbox to10.36pt{\vbox to10.36pt{\pgfpicture\makeatletter\hbox{\hskip 5.17923pt\lower-5.17923pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }{}\pgfsys@moveto{4.97923pt}{0.0pt}\pgfsys@curveto{4.97923pt}{2.74998pt}{2.74998pt}{4.97923pt}{0.0pt}{4.97923pt}\pgfsys@curveto{-2.74998pt}{4.97923pt}{-4.97923pt}{2.74998pt}{-4.97923pt}{0.0pt}\pgfsys@curveto{-4.97923pt}{-2.74998pt}{-2.74998pt}{-4.97923pt}{0.0pt}{-4.97923pt}\pgfsys@curveto{2.74998pt}{-4.97923pt}{4.97923pt}{-2.74998pt}{4.97923pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.7989pt}{-2.39166pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\hskip 1.13809pt\scriptsize\!I}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\mid h\in G\} which are not singletons.. Notice that may have no objects and/or no attributes. More precisely, if is the apposition (subposition) of a contranominal scale and a full context, then will have no objects (attributes). In particular, if is a contranominal scale, its noncontranominal kernel will not have any objects or attributes. Lastly, we define to be the set of contexts in which have the maximum number of concepts (among all contexts in ).
Theorem 5**.**
Amongst the contexts with objects, attributes and no contranominal-scale of size , there exists one context with maximum number of concepts which has a contranominal-scale of size as a subcontext.
Proof.
For an arbitrary context , let be its noncontranominal kernel. We define the following non-deterministic operation .
[TABLE]
It should be clear that has always at least as many concepts as . Moreover, is either itself or increases by exactly one. We claim that
[TABLE]
Indeed, consider a maximum contranominal scale . We may suppose , thus, a pair was chosen by the operation . If both and are inside , then clearly . If neither nor are inside , then obviously . If only one among and are inside , then there exists a contranominal scale of size with neither nor . Hence, and will, together, belong to a in . This proves the lower bound . The upper bound is clear.
Let . Consider the nondeterministic sequence
[TABLE]
The last context in the sequence above that still belongs to must have as a subcontext. Its extremality follows from the extremality of . ∎
A natural way of attacking this question aiming to prove the full conjecture would be trying to prove that a “smart” choice of done by Corollary 1 actually achieves . The context depicted in Figure 8, though, is “resistant” to such idea. Actually, for any choice of and , the resulting context is such that (ConExp or similar comes in handy).
The reference list from the paper itself. Each links out to its DOI / PubMed record.
- 1[Bol 78] Béla Bollobás. Extremal graph theory . Academic Press, 1978.
- 2[GW 99] Bernhard Ganter and Rudolf Wille. Formal Concept Analysis: Mathematical Foundations . Springer, Berlin-Heidelberg, 1999.
