NNRat not countable?

Stream: new members

[Joris van Winden]

I am writing a probability proof, and I want to use ae_all_iff on a statement of the form h : ∀ c : ℚ≥0, ∀ᵐ ω ∂P, M c where M is some predicate. In my case M essentially consists of a bunch of bounds formulated for ℝ≥0, so I would really like to have c range over a type which coerces nicely to ℝ≥0.

The problem that I encounter is that lean cannot synthesize Countable ℚ≥0, even though this intuitively seems like it should be true. Why is this happening, and is there a good way to work around this?

[Ruben Van de Velde]

Doesn't seem to be there, let me check if I can prove it in a few minutes

[Aaron Liu]

import Mathlib

theorem NNRat.countable : Countable NNRat :=
  Subtype.countable

[Ruben Van de Velde]

That's even shorter than mine

instance : Countable ℚ≥0 :=
  (Function.invFun_surjective NNRat.coe_injective).countable

[Ruben Van de Velde]

Aaron, can you please PR yours?

[Joris van Winden]

Thanks! So I guess this is currently just missing from mathlib then?

[Ruben Van de Velde]

Yes

[Ruben Van de Velde]

I think NNRat hasn't seen that much use yet

[Aaron Liu]

#33749

[Etienne Marion]

I once got into this issue as well, I needed a countable dense subset of NNReal, but I realized that using an arbitrary one was just easier than using the range of the coercion NNRat -> NNReal.

[Aaron Liu]

do we have a TopologicalSpace.SeparableSpace instance?

[Etienne Marion]

Yes, I used TopologicalSpace.exists_countable_dense here.

[Etienne Marion]

NNReal.instSecondCountableTopology

[Joris van Winden]

Etienne Marion said:

I once got into this issue as well, I needed a countable dense subset of NNReal, but I realized that using an arbitrary one was just easier than using the range of the coercion NNRat -> NNReal.

Ah, thanks for this suggestion. I'm having some additional difficulty managing various coercions between ℚ, ℝ and their nonnegative variants, so I might try this approach instead.