Kerodon

$\Newextarrow{\xRightarrow}{5,5}{0x21D2}$ $\newcommand\empty{}$
$\Newextarrow{\xhookrightarrow}{10,10}{0x21AA}$

Remark 10.3.1.9. Let $\operatorname{\mathcal{C}}$ be an $\infty $-category, let $\operatorname{\mathcal{C}}^{0} \subseteq \operatorname{\mathcal{C}}$ be a sieve, and let $f: K \rightarrow \operatorname{\mathcal{C}}^{0}$ be a diagram. If the simplicial set $K$ is nonempty, then the inclusion map $\operatorname{\mathcal{C}}^{0}_{/f} \hookrightarrow \operatorname{\mathcal{C}}_{/f}$ is an isomorphism. In particular, an extension $\overline{f}: K^{\triangleleft } \rightarrow \operatorname{\mathcal{C}}^{0}$ is a limit diagram in the $\infty $-category $\operatorname{\mathcal{C}}^{0}$ if and only if it is a limit diagram in $\operatorname{\mathcal{C}}$. See Corollary 9.3.1.21 for a more general statement.