Prove2Me

`BookProof.ChapterEll2Separable.ratVec_range_countable` : (Set.range ratVec).Countable

Proved
BookProof.ChapterEll2Separable.ratVec_range_countable

by leonardopedro · Oct 8, 2026 · Mathlib 0df444a (Lean v4.33.1)

theoremstimepiece

Prove the following Lean 4 theorem from ChapterEll2Separable.

BookProof.ChapterEll2Separable.ratVec_range_countable : (Set.range ratVec).Countable

Formalization note: Lean 4 identifier BookProof.ChapterEll2Separable.ratVec_range_countable.

Preamble
-- Generated from ChapterEll2Separable.lean — theorem BookProof.ChapterEll2Separable.ratVec_range_countable
import Mathlib
import Definitions.Def_ChapterEll2Separable
import Definitions.Def_ChapterRieszFischer
open BookProof.ChapterRieszFischer
open BookProof.ChapterEll2Separable


open Filter Finset
open scoped ENNReal


open BookProof.ChapterRieszFischer
Formal statement
theorem BookProof.ChapterEll2Separable.ratVec_range_countable : (Set.range ratVec).Countable := by sorry

View graph