无法获取变量

Question

我正在尝试证明我提出的以下简单定理：

A point is on the boundary iff any small enough ball around that point contains points both in S and out of S.

下面我已经设法做到了向前的方向，但我被困在向后的方向上。

在最后一步使用相同的方法失败，目标很接近但还没有完全实现，我不知道该怎么做：

lemma frontier_ball: "x ∈ frontier S ⟷
  (∃r>0. (∀δ>0. δ<r ⟶ ((ball x δ) ∩ S ≠ {} ∧ (ball x δ) ∩ -S ≠ {})))"
  (is "?lhs = ?rhs")
proof
  {
    assume "?lhs"
    hence "x ∉ interior S ∧ x ∉ interior (-S)" by (auto simp: frontier_def interior_complement)
    hence "∀δ>0. ((ball x δ) ∩ S ≠ {} ∧ (ball x δ) ∩ -S ≠ {})" by (auto simp: mem_interior)
    then have "?rhs" by (simp add: Orderings.no_top_class.gt_ex)
  }
  {
    assume "¬?lhs"
    hence "x ∈ interior S ∨ x ∈ interior (-S)" by (auto simp: frontier_def interior_complement)
    hence "∃δ>0. ball x δ ∩ S = {} ∨ ball x δ ∩ -S = {}" by (auto simp: mem_interior)
    then have "¬?rhs" by (simp add: subset_ball)
  }
qed

我试图告诉伊莎贝尔如何获得这样的增量，但它卡在了获取步骤上：

lemma frontier_ball: "x ∈ frontier S ⟷
  (∃r>0. (∀δ>0. δ<r ⟶ ((ball x δ) ∩ S ≠ {} ∧ (ball x δ) ∩ -S ≠ {})))"
  (is "?lhs = ?rhs")
proof
  {
    assume "?lhs"
    hence "x ∉ interior S ∧ x ∉ interior (-S)" by (auto simp: frontier_def interior_complement)
    hence "∀δ>0. ((ball x δ) ∩ S ≠ {} ∧ (ball x δ) ∩ -S ≠ {})" by (auto simp: mem_interior)
    then have "?rhs" by (simp add: Orderings.no_top_class.gt_ex)
  }
  {
    fix r::real
    assume "¬?lhs ∧ r>0"
    hence "x ∈ interior S ∨ x ∈ interior (-S)" by (auto simp: frontier_def interior_complement)
    then obtain r2 where "r2>0" and "ball x r2 ∩ S = {} ∨ ball x r2 ∩ -S = {}" by (auto simp: mem_interior)
    then obtain δ where "δ>0 ∧ δ<r ∧ δ<r2" by auto

  }
qed

任何指点都会很棒！

Answer 1

嗯，你可以构造这样一个δ。如果你有 r > 0 和 r2 > 0，你想要一些 δ 来满足 0 < δ ≤ r2 和 0 < δ < r，为什么不直接使用 min r2 (r/2)？您可以将 δ 定义为那个，然后您可以证明您想要的属性：

    def δ ≡ "min r2 (r/2)"
    with r2 A have δ: "δ > 0" "δ < r" "δ ≤ r2" by auto
    with r2 have δ': "ball x δ ∩ S = {} ∨ ball x r2 ∩ -S = {}" using subset_ball[OF δ(3)] by auto

或者更直接一点：

lemma frontier_ball: "(x :: 'a :: {metric_space}) ∈ frontier S ⟷
  (∃r>0. (∀δ>0. δ<r ⟶ ((ball x δ) ∩ S ≠ {} ∧ (ball x δ) ∩ -S ≠ {})))"
  (is "?lhs = ?rhs")
proof -
  {
    assume "?lhs"
    hence "x ∉ interior S ∧ x ∉ interior (-S)" by (auto simp: frontier_def interior_complement)
    hence "∀δ>0. ((ball x δ) ∩ S ≠ {} ∧ (ball x δ) ∩ -S ≠ {})" by (auto simp: mem_interior)
    then have "?rhs" by (simp add: Orderings.no_top_class.gt_ex)
  }
  moreover
  {
    assume lhs: "¬?lhs"
    {
      fix r :: real assume r: "r > 0"
      from lhs have "x ∈ interior S ∨ x ∈ interior (-S)" 
        by (auto simp: frontier_def interior_complement)
      then obtain δ where "δ > 0" "ball x δ ∩ S = {} ∨ ball x δ ∩ -S = {}" 
        by (auto simp: mem_interior)
      with r have "min δ (r/2) > 0" "min δ (r/2) < r" 
        "ball x (min δ (r/2)) ∩ S = {} ∨ ball x (min δ (r/2)) ∩ -S = {}" using subset_ball by auto
      hence "∃δ>0. δ < r ∧ (ball x δ ∩ S = {} ∨ ball x δ ∩ -S = {})" by blast
    }
    hence "¬?rhs" by blast
  }
  ultimately show ?thesis by blast
qed

郑重声明，我会避免做 assume "A ∧ B" 这样的事情。改为执行 assume "A" "B"。这为您提供了两个可以直接使用的事实，而不是让它们在一个事实中用 HOL 连词包裹起来。

无法获取变量

Can't obtain variable

isabelle