在上一个问题中，我询问了关于形式化欧几里得空间子集的问题，我收到了以下关于如何创建 n 维欧几里得空间的回复：
def euclidean_space (n : ℕ) : Type := set (repeated_prod n ℝ)
我收到了以下关于创建欧几里得空间子集的回复：
def euclidean_subset (M : Type) := ∃ (n : ℕ) (P : euclidean_space n → Prop), M = subtype P
运行我修改后的代码，编译的所有内容都很棒，并且相信答案（至少，大部分）是正确的。我想尝试对代码进行一些基本检查。特别是，我希望：
#reduce euclidean_space 2
给：
ℝ × ℝ
好吧，它没有。它超时了。然后我继续尝试其他一些套装。我修改euclidean_space为：
def euclidean_space (n : ℕ) : Type := set (repeated_prod n ℕ)
虽然，不再忠实于它的名字，人们应该期待
#reduce euclidean_space 2
给：
ℕ × ℕ
好吧，几乎，它给出了：
ℕ × ℕ → Prop
鉴于结果我删除了set调用并重新定义euclidean_space为：
def euclidean_space (n : ℕ) : Type := (repeated_prod n ℕ)
减少产生了预期的结果。然后我返回并用ℝ替换了ℕ：
def euclidean_space (n : ℕ) : Type := (repeated_prod n ℝ)
euclidean_subset仍然编译，但是#reduce仍然使用 ℝ 给出超时。为什么ℕ不超时？