All
$$f(x) \;\text{ for all } x \in S$$
True if $f(x)$ is true for all $x$ in $S$, and false otherwise.
$$f(x) \;\text{ for all } x \in S \text{ with } P(x)$$
True if $f(x)$ is true for all $x$ in $S$ satisfying the condition $P(x)$, and false otherwise.
$${e}^{x} \ge 1 \;\text{ for all } x \in \mathbb{R} \text{ with } x \ge 0$$
An example of a quantified formula.
$$\left(x \ge 0\right) \implies \left({e}^{x} \ge 1\right) \;\text{ for all } x \in \mathbb{R}$$
Logically equivalent to the previous example.
$$\left(x \in \mathbb{R} \;\mathbin{\operatorname{and}}\; x \ge 0\right) \implies \left({e}^{x} \ge 1\right) \;\text{ for all } x$$
Normally, the domain of the bound variable should be specified with a ForElement expression, but a raw For(x) can be used to quantify over the entire universe. This form is acceptable when the Implies expression contains a domain statement.
$$\left(P(x) \;\text{ for all } x \in S\right) \iff \left(\operatorname{False} \notin \left\{ P(x) : x \in S \right\}\right)$$
Equivalent characterization of this operator.
Input: Equivalent(All(P(x), ForElement(x, S), Q(x)), NotElement(False, Set(P(x), ForElement(x, S), Q(x))))
$$\left(P(x) \;\text{ for all } x \in S \text{ with } Q(x)\right) \iff \left(\operatorname{False} \notin \left\{ P(x) : x \in S \,\mathbin{\operatorname{and}}\, Q(x) \right\}\right)$$Equivalent characterization of this operator.
Last updated: 2020-03-06 00:22:16