Set α ≠ α

Stream: mathlib4

[Mac Malone]

I have learned that ∀ α, Set α ≠ α is not a theorem in mathlib (at least according to a Loogle search). Is this something worth contributing? More generally, are such theroerems about types in scope of mathlib?

[Kyle Miller]

That one can be strengthened to saying that the types are not equivalent. I'm pretty sure that exists somewhere, but I don't remember what it's called...

[Kyle Miller]

At least there's docs#Function.cantor_surjective and docs#Function.cantor_injective

[Kyle Miller]

example {α : Type _} (h : Set α = α) : False :=
  Function.cantor_injective (cast h) (by intro; simp)

[Mac Malone]

Yeah, that is essentially my proof. :wink:

[Mac Malone]

I didn't realize the proof for the injectivity of the cast could be reduced to by intros; ismp, though. Instead, I proved cast_injective (which I also could not find in Lean/mathlib) as well.

[Kyle Miller]

I think cast_injective would be great to contribute. I was just about to suggest it :-)

[Kyle Miller]

by intro; simp is just a trick that happened to work.

[Eric Wieser]

Maybe this spelling of the statement?

import Mathlib

namespace Cardinal

theorem card_lt_card_set {α : Type*} : #α < #(Set α) := by
  rw [← Cardinal.mk_embedding_eq_zero_iff_lt, mk_eq_zero_iff, isEmpty_iff]
  rintro ⟨_, hf⟩
  exact Function.cantor_injective _ hf

[Eric Wieser]

Though I guess docs#Cardinal.cantor is close enough

[Mac Malone]

Kyle Miller said:

I think cast_injective would be great to contribute. I was just about to suggest it :-)

Apparently this alredy does somewhat exist as cast_inj, which is not quite Injective (cast h) (and which is why I did not find it in my search).

[Mac Malone]

(I learned this with a simp? on your example.)

[Kyle Miller]

Eric Wieser said:

Though I guess docs#Cardinal.cantor is close enough

Yeah:

theorem card_lt_card_set {α : Type*} : #α < #(Set α) := by
  rw [mk_set]
  apply Cardinal.cantor

[Kyle Miller]

@Mac Malone Usually there's foo_injective for the Injective version and foo_inj for the spelled-out version. I think we should have cast_injective and cast_surjective.

[Violeta Hernández]

Equality of types is often not a useful notion. About as much as you can ask about two distinct types is whether there exists an equivalence or not.

[Violeta Hernández]

(which is what this cardinality statement is saying)

[Mac Malone]

While fair and usually true, I happened to be toying around with something where the equality (and inequality) of types was of prime importance. (An encoding of inductives as types rather than values.)

[Kevin Buzzard]

The only way we can prove that two types are unequal is by proving that they're not equivalent (ie don't biject with each other). For example Nat = Int is undecidable. This is the main reason why equality of types is not fleshed out in mathlib -- it's just a weaker version of equality of cardinality if it's not rfl