AI 中文总结
该论文在ZFC公理系统中证明了当离散拓扑空间D的基数为ℵ₁时，与离散拓扑兼容的度量空间Met(D)不是完全可度量化的，且证明已在Lean 4中形式化。
AI 中文摘要
对于离散拓扑空间D，令Met(D)表示D上与离散拓扑兼容的度量构成的集合，配备由上确界距离诱导的拓扑。石木猜想5.1断言，当|D|=ℵ₁时，Met(D)不是完全可度量化的。我们在ZFC公理系统中通过构造一个基数为ℵ₁且不是F_σ集的集合A⊆[0,1]，并将其补集作为闭子空间嵌入Met(D)来证明该猜想，该证明已在Lean 4中形式化。
英文摘要
For a discrete topological space $D$, let $\mathrm{Met}(D)$ denote the set of metrics on $D$ that are compatible with the discrete topology, equipped with the topology induced by the supremum distance. Ishiki's Conjecture 5.1 asserts that $\mathrm{Met}(D)$ is not completely metrizable when $\lvert D\rvert = \aleph_1$. We prove this in ZFC by constructing a set $A \subseteq [0,1]$ of cardinality $\aleph_1$ that is not $F_σ$ and embedding its complement as a closed subspace of $\mathrm{Met}(D)$. The proof has also been formalised in Lean 4.
Comments8 pages; the proof has also been formalised in Lean 4
