## Stream: Is there code for X?

### Topic: manipulating multiset elements in proof

#### Bassem Safieldeen (Jul 26 2020 at 11:11):

Hi everyone,

I am learning how to do stuff with multisets and I am stuck. I have a multiset X : multiset ℝ and a function myFunc : multiset ℝ → multiset ℝ that doubles elements of a multiset. I am trying to prove that if the multiset has 10 elements and each element of the multiset is 5, then applying myFunc and summing gives us 100.

Here is my code:

import algebra.big_operators
import data.real.basic

/-
A function that doubles every element in a given multiset of ℝ.
-/
def myFunc : multiset ℝ → multiset ℝ :=
begin
intro X,
exact multiset.map (λ x:ℝ, 2*x) X,
end

/-
For a multiset of 10 elements, all of which are 5, doubling
each element and summing gives 100.
-/
example (X : multiset ℝ) (hX' : X.card = 10) :
(∀(x:ℝ), x ∈ X → x = 5) → (myFunc X).sum = 100  :=
begin
intro hX'',
unfold myFunc,
--  ⊢ (multiset.map (λ (x : ℝ), 2 * x) X).sum = 100
sorry
end


#### Mario Carneiro (Jul 26 2020 at 11:12):

The first step might be to prove X = list.repeat 5 10

#### Bassem Safieldeen (Jul 26 2020 at 11:16):

Mario Carneiro said:

The first step might be to prove X = list.repeat 5 10

Will give it a try now.

#### Kenny Lau (Jul 26 2020 at 11:17):

import algebra.big_operators
import data.real.basic

/-
A function that doubles every element in a given multiset of ℝ.
-/
def myFunc (X : multiset ℝ) : multiset ℝ :=
X.map $λ x, 2 * x theorem multiset.map_repeat {α β : Sort*} (f : α → β) (x : α) (n : ℕ) : (multiset.repeat x n).map f = multiset.repeat (f x) n := nat.rec_on n rfl$ λ n ih, by simp_rw [multiset.repeat_succ, multiset.map_cons, ih]

/-
For a multiset of 10 elements, all of which are 5, doubling
each element and summing gives 100.
-/
example (X : multiset ℝ) (hX1 : X.card = 10) (hX2 : ∀ x ∈ X, (x : ℝ) = 5) : (myFunc X).sum = 100 :=
by { rw [multiset.eq_repeat_of_mem hX2, hX1, myFunc, multiset.map_repeat, multiset.sum_repeat], norm_num }


#### Kenny Lau (Jul 26 2020 at 12:26):

That means f \$ x y = f (x y) (as opposed to f x y = (f x) y)

#### Eric Wieser (Jul 29 2020 at 18:20):

(deleted)

Last updated: May 16 2021 at 05:21 UTC