# Zulip Chat Archive

## Stream: general

### Topic: heq

#### Sebastien Gouezel (Apr 09 2020 at 19:21):

Suppose that I have `f : fin k -> alpha`

and `g : fin n -> alpha`

, and I know `f == g`

. Can I deduce `k = n`

?

#### Chris Hughes (Apr 09 2020 at 19:26):

I think only if `alpha`

is finite and has cardinality at least 2. You know the types are equal, but types with the same cardinality are not provably unequal.

#### Chris Hughes (Apr 09 2020 at 19:28):

If nonempty types are equal, then they must have a pair of elements that are `heq`

.

#### Yury G. Kudryashov (Apr 09 2020 at 19:29):

It's `fin k`

and `fin n`

, so their cardinalities are the same only if `k = n`

.

#### Sebastien Gouezel (Apr 09 2020 at 19:35):

Yes, if `alpha`

is finite I can do it by cardinality arguments. I guess that if `alpha`

is infinite then this does not follow from Lean's axioms, but I might be wrong on this.

#### Yury G. Kudryashov (Apr 09 2020 at 19:36):

Ah, it's `fin k → α`

, not `fin k`

.

#### Yury G. Kudryashov (Apr 09 2020 at 19:36):

I should read more carefully.

#### Yury G. Kudryashov (Apr 09 2020 at 19:37):

And think before typing.

#### Kevin Buzzard (Apr 09 2020 at 19:41):

You're a mathematician so if you have `f == g`

then you already went wrong somewhere earlier, right?

#### Sebastien Gouezel (Apr 09 2020 at 20:00):

No, it's when building an equiv between some objects, you start from a function `fin k -> alpha`

, then you apply `to_fun`

, then `inv_fun`

, and in the end you get a function `fin n -> alpha`

, and you need to prove that it is the same function as the one you started with. You get into `==`

quickly with this, but it's not really bad, you can prove that `k = n`

and then do `induction`

on the equality and you are back on track. If I could have deduced `k = n`

from `f == g`

, this would have saved me a few lines, but I can prove it directly in my context.

#### Kevin Buzzard (Apr 09 2020 at 20:01):

I was in this situation with quotient groups at some point in the perfectoid project and just proved some stupid lemmas, like e.g. I defined a map from G/N to G/K if K and N were normal subgroups and N=K(!)

Last updated: May 11 2021 at 14:11 UTC