This is for actual research, but at a rather basic level of maths, so I am not sure if it goes here or on MO. Oh well.
I am trying to find if there is an established name for the following property of a subset of a poset: every element is under a maximal element. In other words, the union of the lower sets of the maximal elements includes the original set. Formally:
$$ \forall x \in X. \exists y \in X. [\forall y' \in X. y \leq y' \rightarrow y = y'] \land x \leq y $$
This feels like a rather basic notion but I was unable to find references to it, hence my asking. I am not sure if it might be related to topological notions (it feels related to closedness?).
The context is that in natural language semantics, we often have an "alternative set" $A$ of propositions (propositions being themselves sets, so it's a set of sets), and I would like to prove an equivalence between two notions defined on such sets; at some point I need to assume that all sets of "true alternatives at a given world", that is, of the form $T(x) = \{p : x \in p, p \in A\}$ for some $x$, have the property in question (under reversed inclusion). I could simply assume that everything is finite, which is usually the case, but there are a few concrete proposals in the literature where the alternative sets are infinite, but still verify this property (with finite numbers of maximal elements). If someone has a name for the property I want as a property of $A$ rather than a property of $T(x)$, I am interested too.