A set of integers "same" as a set of reals

Stream: new members

[Tony Ma]

I have been told that LEAN treats $\mathbb{Z}$ and $\mathbb{R}$ as different types (if I made the correct phrase). Therefore, $\mathbb{Z}$ is not regarded as a subset of $\mathbb{R}$, but casting are often required instead. However, I wonder what could I do in order to prove something like this:

have h : {x : ℝ | ∃ n : ℤ, x = n}.encard = {n : ℤ | True}.encard := by sorry

or this:

have g : {x : ℝ| -2 ≤ x ∧ x ≤ 2}.ncard = {x : ℤ| -2 ≤ x ∧ x ≤ 2}.ncard := by sorry

Any help would be appreciated!

[Riccardo Brasca]

You can just build a bijection between the two sets.

[Riccardo Brasca]

For example, for the first one

import Mathlib

def φ : {n : ℤ | True} → {x : ℝ | ∃ n : ℤ, x = n} := fun n ↦ ⟨n.1, n, rfl⟩

example : {x : ℝ | ∃ n : ℤ, x = n}.encard = {n : ℤ | True}.encard := by
  refine (Set.encard_congr (Equiv.ofBijective φ ⟨fun a b hab ↦ ?_, fun ⟨a, b, h⟩ ↦
    ⟨⟨b, trivial⟩, ?_⟩⟩)).symm
  · simp [φ] at hab
    exact SetCoe.ext hab
  · exact SetCoe.ext h.symm

[Tony Ma]

@Riccardo Brasca Thank you! But what does ⟨n.1, n, rfl⟩ means? (Especially, what does n.1 means?) And what if I wanted to create a bijection in reverse way (i.e. function of real numbers to integers)?

[Daniel Weber]

The second one isn't true - the first set is infinite, while the second has 5 members

[Matt Diamond]

@Tony Ma Here's an example of a bijection in the reverse way (from Real Integers to Integers, using types/subtypes instead of sets):

import Mathlib

open Function Cardinal

-- The subtype of Real Integers
def RealInt : Type := { r : ℝ // r ∈ Set.range Int.cast }

noncomputable
def real_to_int (x : RealInt) : ℤ := x.property.choose

lemma real_to_int_spec (x : RealInt) : Int.cast (real_to_int x) = x.val := x.property.choose_spec

lemma real_to_int_inj : Injective real_to_int :=
by
  intro a b h
  replace h := congrArg (Int.cast (R := ℝ)) h
  simpa [real_to_int_spec, Subtype.val_inj] using h

lemma real_to_int_surj : Surjective real_to_int :=
by
  intro x
  use ⟨Int.cast x, Set.mem_range_self _⟩
  simp [real_to_int]

lemma real_to_int_bij : Bijective real_to_int :=
⟨real_to_int_inj, real_to_int_surj⟩

noncomputable
def RealInt_equiv_Int : RealInt ≃ ℤ :=
Equiv.ofBijective real_to_int real_to_int_bij

-- Real Integers have the same cardinality as the Integers
example : #RealInt = #ℤ := RealInt_equiv_Int.cardinal_eq

[Ruben Van de Velde]

For n a value of type {n : ℤ | True} (coerced to a type), n.1 is the underlying value of type ℤ

[Tony Ma]

Matt Diamond 发言道：

Tony Ma Here's an example of a bijection in the reverse way (from Real Integers to Integers, using types/subtypes instead of sets):

import Mathlib

open Function Cardinal

-- The subtype of Real Integers
def RealInt : Type := { r : ℝ // r ∈ Set.range Int.cast }

noncomputable
def real_to_int (x : RealInt) : ℤ := x.property.choose

lemma real_to_int_spec (x : RealInt) : Int.cast (real_to_int x) = x.val := x.property.choose_spec

lemma real_to_int_inj : Injective real_to_int :=
by
  intro a b h
  replace h := congrArg (Int.cast (R := ℝ)) h
  simpa [real_to_int_spec, Subtype.val_inj] using h

lemma real_to_int_surj : Surjective real_to_int :=
by
  intro x
  use ⟨Int.cast x, Set.mem_range_self _⟩
  simp [real_to_int]

lemma real_to_int_bij : Bijective real_to_int :=
⟨real_to_int_inj, real_to_int_surj⟩

noncomputable
def RealInt_equiv_Int : RealInt ≃ ℤ :=
Equiv.ofBijective real_to_int real_to_int_bij

-- Real Integers have the same cardinality as the Integers
example : #RealInt = #ℤ := RealInt_equiv_Int.cardinal_eq

Thank you!