fix bold space

interacting_with_lean.md

@@ -74,7 +74,7 @@ Importing is transitive. In other words, if you import ``Foo`` and ``Foo`` impor
 then you also have access to the contents of ``Bar``, and do not need to import it explicitly.
 -->
 
-导入文件 ``Bar/Baz/Blah.olean``，其中的描述是相对于Lean **搜索路径** 解释的。关于如何确定搜索路径的信息可以在[文档](https://lean-lang.org/documentation/)中找到。默认情况下，它包括标准库目录，以及（在某些情况下）用户的本地项目的根目录。
+导入文件 ``Bar/Baz/Blah.olean``，其中的描述是相对于 Lean **搜索路径** 解释的。关于如何确定搜索路径的信息可以在[文档](https://lean-lang.org/documentation/)中找到。默认情况下，它包括标准库目录，以及（在某些情况下）用户的本地项目的根目录。
 
 导入是传递性的。换句话说，如果你导入了 ``Foo``，并且 ``Foo`` 导入了 ``Bar``，那么你也可以访问 ``Bar`` 的内容，而不需要明确导入它。