Proving Countability of linear equivalences

Stream: new members

[Rahul Soni]

Hello Everyone, any pointers on solving this :-

import Mathlib
variable (h : ℕ → ℝ)
def isLinearCombination(a1 : ℝ)(a2 : ℝ) : Prop :=
    ∃ l : ℕ →₀ ℤ  , a1 - a2 =  ∑ i ∈ l.support, l i • h i

instance LinCombEquiv : Equivalence (isLinearCombination h) := sorry

instance SR : Setoid ℝ where
  r := isLinearCombination h
  iseqv := LinCombEquiv h

def E : (Quotient (SR h)) → Set ℝ := λ x => {y : ℝ | x = ⟦y⟧}

/-We specify that each equivalence class is countable -/
theorem EalphaCountable (α : Quotient (SR h)) : ((E h) α).Countable := by
  rw[E,←Set.countable_coe_iff,countable_iff_exists_injective]
  sorry

I am stuck on proving that it's countable.

[Kevin Buzzard]

What's the maths proof which you want to formalize?

[Rahul Soni]

First, we need to show that there are only countably many Finitely supported functions then every element can be rewritten as the sum of the default element and the evaluation of the finitely supported function on h

[Andrew Yang]

I think the more mathliby way to write these definitions is

import Mathlib
variable (h : ℕ → ℝ)

open Set Submodule

/-We specify that each equivalence class is countable -/
theorem EalphaCountable (α : ℝ ⧸ span ℤ (range h)) : (Submodule.Quotient.mk ⁻¹' {α}).Countable := by

and you might find more lemmas this way.