Cardinality as a real number

Stream: new members

[Bjørn Kjos-Hanssen]

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]

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]

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

[Bjørn Kjos-Hanssen]

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]

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]

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]

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]

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]

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]

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]

That did it!