## Stream: new members

### Topic: Cardinality as a real number

#### Bjørn Kjos-Hanssen (Oct 26 2020 at 01:23):

I want to do this:

parameter M :  ℝ
def test : finset ℕ → ℝ := λ A, M * (A.card)


But there is an error concerning decidable_linear_order ℝ not being the same type as ℝ.
I also tried with ↑(A.card) but that didn't fix it. :cant_talk:

#### Heather Macbeth (Oct 26 2020 at 01:38):

I actually don't know what a parameter is. Is there a reason not to use variable? This seems to work:

import data.real.basic

variable (M : ℝ)

def test : finset ℕ → ℝ := λ A, M * A.card


#### Bjørn Kjos-Hanssen (Oct 26 2020 at 01:42):

Oh that's strange... parameter was in order to not have to mention M all the time

#### Bjørn Kjos-Hanssen (Oct 26 2020 at 01:47):

Well, using variable causes another error:

import data.real.basic

variable (M : ℝ)

def test : finset ℕ → ℝ := λ A, M * A.card

theorem test_thm {A : finset ℕ}: test A = test A, from sorry


The error is

type mismatch at application  test A term  A has type  finset ℕ but is expected to have type  ℝ


I guess I would have to write test M Ainstead of test M.
Thanks though, I might give in and do that.

#### Yakov Pechersky (Oct 26 2020 at 02:04):

Not sure what exactly you want to do. Hard to guess without a #mwe. Usually, parameter is not what you want. But here is a "mwe":

import data.real.basic

section

parameter M : ℝ

def test : finset ℕ → ℝ := λ A, M * (A.card)

end


#### Yakov Pechersky (Oct 26 2020 at 02:05):

Specifically, this will still make test take some real as the first argument:

import data.real.basic

section

parameter M : ℝ

def test : finset ℕ → ℝ := λ A, M * (A.card)

end

#check test
/-
test : ℝ → finset ℕ → ℝ
-/


#### Bjørn Kjos-Hanssen (Oct 26 2020 at 02:44):

I thought maybe the point is that f(x,y)=x*y is a computable function but for a given noncomputable c, g(y)=c*y is not computable... but I think the same problem happens with ℚ where all elements are computable.

#### Yakov Pechersky (Oct 26 2020 at 02:52):

I'm not sure what you mean here. I guess I don't know where you were seeing the decidable linear order issue previously

#### Bjørn Kjos-Hanssen (Oct 26 2020 at 05:33):

Thanks @Yakov Pechersky @Heather Macbeth I made some progress from your hints. Now I'm stuck on trying to prove this:

  X.card ≤ Y.card →  ↑( X.card) ≤ ↑(Y.card)


Seems "obvious"...

#### Heather Macbeth (Oct 26 2020 at 05:36):

Great! Do you know about norm_cast and push_cast?
https://leanprover-community.github.io/mathlib_docs/tactics.html#norm_cast

#### Bjørn Kjos-Hanssen (Oct 26 2020 at 05:47):

That did it!

Last updated: May 17 2021 at 21:12 UTC