在Lean中无需选择公理，如何从exists_unique构造定义内的元素？

要构造这个良定义的函数，核心是利用∃!u, P V u的唯一性——这个条件保证了满足P V u的元素是唯一确定的，因此不需要依赖选择公理就能直接提取该元素。以下是两种可行的实现方式：

方法一：直接使用exists_unique.elim #

exists_unique.elim可以直接拆解“存在唯一元素”的命题，提取出该元素并利用唯一性确保返回值的确定性：

variables {Ω : Type} (P:set Ω → Ω → Prop)(a:Ω)

def G :set Ω → Ω:=
begin
  intro V,
  by_cases h: ∃!u : Ω, P V u,
  -- 存在唯一u时，提取该u作为返回值
  { exact exists_unique.elim h (λ u _ _, u) },
  -- 不存在时返回预设的a
  { exact a },
end

方法二：模式匹配拆解exists_unique #

Lean的rcases命令可以直接对exists_unique类型的命题做模式匹配，拆分出元素、元素满足条件的证明，以及唯一性条件，然后直接返回该元素：

variables {Ω : Type} (P:set Ω → Ω → Prop)(a:Ω)

def G :set Ω → Ω:=
begin
  intro V,
  by_cases h: ∃!u : Ω, P V u,
  {
    -- 拆分∃!u为：u本身、P V u的证明、唯一性条件
    rcases h with ⟨u, h_P, h_unique⟩,
    exact u,
  },
  { exact a },
end

为什么不需要选择公理？ #

选择公理用于处理“仅知道存在元素，但不唯一”的场景，需要从多个候选元素中任意选择一个。而这里的∃!u已经保证了元素的唯一性，我们不需要“选择”，直接取那个唯一确定的元素即可，因此整个构造是构造性的，不依赖选择公理。

内容的提问来源于stack exchange，提问作者Vicent Pons llopis