Given any proposition <math>f : X \to \mathbb{B},</math> the ''tacit extension'' of <math>f\!</math> to <math>\operatorname{E}X</math> is notated <math>\varepsilon f : \operatorname{E}X \to \mathbb{B}</math> and defined by the equation <math>\varepsilon f = f,</math> so it's really just the same proposition living in a bigger universe.
−
Given any proposition f : X -> B, the "tacit extension" of f to EX
−
is notated !e!f : EX -> B and defined by the equation !e!f = f, so
−
it's really just the same proposition living in a bigger universe.
−
Tacit extensions formalize the intuitive idea that a new function
+
Tacit extensions formalize the intuitive idea that a new function is related to an old function in such a way that it obeys the same constraints on the old variables, with a "don't care" condition on the new variables.
−
is related to an old function in such a way that it obeys the same
−
constraints on the old variables, with a "don't care" condition on
−
the new variables.
−
Figure 24-2 illustrates the "tacit extension" of the proposition
+
Figure 24-2 illustrates the tacit extension of the proposition or scalar field <math>f = pq : X \to \mathbb{B}</math> to give the extended proposition or differential field that we notate as <math>\varepsilon f = \varepsilon (pq) : \operatorname{E}X \to \mathbb{B}.</math>
−
or scalar field f = pq : X -> B to give the extended proposition
−
or differential field that we notate as !e!f = !e![pq] : EX -> B.