## Stream: general

### Topic: function on sums

#### j_lean (Jun 26 2019 at 21:57):

Hi all,

I need to define a function on a sum of two types in a proof, but I am not sure how to do it. Does anyone know how to do that?

I'd like to prove this theorem:

theorem sumfunc: ∃ f : sum ℕ ℤ → ℕ, ∀ a : ℕ, f (sum.inl a) = 0 ∧ ∀ b : ℤ, f (sum.inr b) = 1 :=

The function should be f x = 0 if x : \nat and f x = 1 if x : \int. I have used the tactic "existsi", but I am not successful.

Although I can't define the function inside the proof, but I can define it as a definition in Lean. Here it is:

definition f (x : sum ℕ ℤ) : ℕ := sum.cases_on x (λ x, 0) (λ x, 1).

Thanks.

#### Reid Barton (Jun 26 2019 at 21:59):

What did you try that involved existsi?

#### Kenny Lau (Jun 26 2019 at 22:00):

theorem sumfunc : ∃ f : sum ℕ ℤ → ℕ, (∀ a : ℕ, f (sum.inl a) = 0) ∧ (∀ b : ℤ, f (sum.inr b) = 1) :=
⟨sum.rec (λ n, 0) (λ n, 1), λ n, rfl, λ n, rfl⟩


#### Kenny Lau (Jun 26 2019 at 22:01):

definition f (x : sum ℕ ℤ) : ℕ := sum.cases_on x (λ x, 0) (λ x, 1)

theorem sumfunc : ∃ f : sum ℕ ℤ → ℕ, (∀ a : ℕ, f (sum.inl a) = 0) ∧ (∀ b : ℤ, f (sum.inr b) = 1) :=
begin
existsi f, split; intros; refl
end


#### j_lean (Jun 28 2019 at 20:20):

Thanks Kenny Lau. It's nice to define the function before the theorem.

Last updated: May 11 2021 at 12:15 UTC