CODEWITHSUNDEEP
mathdefinitionfunction-definitiontheorem-provinglean
Vicent Pons llopis
Vicent Pons llopis

Reputation: 1

In Lean, how can i get the element from an exists_unique in a definition

I want to make the following

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

def G :set Ω → Ω:=
begin
  intro V,
  by_cases h: ∃!u : Ω, P V u,
  --I want to use the u that is unique as return in this case, and in the other case use the a
  sorry,
  exact a,
end

I tried using the exists.elim and exists_unique.elim but i can't figure out how to use them properly, also I can't use h.some because I'm not using the axiom of choice. I just want to know how to construct the function proving it's well defined, thanks.

Upvotes: 0

Views: 508

Answers (1)

Eric
Eric

Reputation: 97555

You can use classical.some h to obtain a witness using the axiom of choice. Note that you are already using the axiom of choice via the by_cases tactic.

If you allow yourself to assume fintype Ω, then you can use fintype.choose h to use brute force instead of an axiom.

Upvotes: 1

Related Questions