A lens shape doimain is defined here as:
Defn A lens-shaped domain $D\subset M$ based on $\Sigma$ is the image of a smooth map $\Phi: \Sigma\times (-1,1) \to M$ where $\Sigma\subset M$ is a compact, codimension 1 submanifold with boundary, with the property that
- $\Phi(\cdot,0):\Sigma\to\Sigma$ is the identity map.
- $\Phi(x,t) = \Phi(x,s)$ for any $x\in\partial\Sigma$, $t,s\in (-1,1)$.
- for any fixed $s\in (-1,1)$, $\Phi(\Sigma, s)$ is a space-like hypersurface.
- away from $\partial\Sigma\times (-1,1)$, $\Phi$ is a diffeomorphism.
The answer to that question from the OP states that the existence of a time function is equivalent to being lens shaped.
I can follow the argument in general. However, I can't see how the condition number two is satisfied from the existence of a time function.
How is the equivalence obtained?
To put it simply: they are not.
When Igor wrote that "the property of being lens-shaped is equivalent to the existence of a smooth time function" in his post, he qualified it with "The main point of confusion, and the reason I did not realize this sooner, is that that the property of a domain being lens-shaped is usually expressed in different terms."
In particular, the types of domain that is considered are more properly compared not with the domain $D$ I wrote in the definition you copied, but with the domain
$$ \mathring{D} := \Phi( (\mathrm{int}(\Sigma) \times (-1,1)) $$
that is to say the boundary $\partial\Sigma$ and its image is excluded. The time function for a lens-shaped domain is simply the coordinate $t\in (-1,1)$. Using the definition that I wrote (which has some technical benefits when it comes to proving energy estimates) you have the problem that $\Phi: \Sigma \times(-1,1) \to M$ is not injective by definition, and so you cannot invert to get the time function.
That condition, however, cannot be simply omitted. The square $(-1,1)\times(-1,1)\subset\mathbb{R}^{1,1}$ in $1+1$ dimensional Minkowski space is generally not considered to be lens-shaped, but it certainly admits a time-function. So you should also read into what Igor wrote as implicitly containing also the requirement "Adding a boundary to compactify $S$, if necessary, and rescaling $f$ to make sure its range is $(−1,1)$" etc. In the context of Lorentzian manifolds, this additional condition can be replaced by requiring the spatial slices to be complete Riemannian manifolds (plus maybe another condition that I forget now; this is almost certainly what Igor had in mind when he invoked Geroch's splitting theorem). But in this case the ambient space $M$ for the domain would have to be the conformal compactification, where the asymptotic infinities are identified appropriately with the boundaries of the spatial slices.