Zulip Chat Archive

Stream: new members

Topic: Cardinality as a real number


view this post on Zulip 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:

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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 ℕ → ℝ
-/

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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"...

view this post on Zulip 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

view this post on Zulip Bjørn Kjos-Hanssen (Oct 26 2020 at 05:47):

That did it!


Last updated: May 17 2021 at 21:12 UTC