theorem MeasurabilityOfFunctions.measurable_generateFrom_iff {X : Type u_1} {Y : Type u_2} [MeasurableSpace X] {G : Set (Set Y)} {f : X → Y} : Measurable f ↔ ∀ A ∈ G, MeasurableSet (f ⁻¹' A)

Lemma 3.1 of Melrose: a function f : X → Y is measurable into the σ-algebra generated by a family G of subsets of Y if and only if the preimages of all generating sets are measurable in X.

theorem MeasurabilityOfFunctions.continuous_imp_measurable {X : Type u_1} {Y : Type u_2} [MetricSpace X] [MetricSpace Y] [MeasurableSpace X] [BorelSpace X] [MeasurableSpace Y] [BorelSpace Y] {f : X → Y} (hf : Continuous f) : Measurable f

Proposition 3.2 of Melrose: between Borel spaces, every continuous map is measurable.

theorem ennrealRatEmbed_dense_Icc (C : ENNReal) (hC : C ≠ ⊤) (ε : ENNReal) (hε : 0 < ε) : ∃ (N : ℕ), ∀ v ≤ C, ∃ k < N, MeasureTheory.SimpleFunc.ennrealRatEmbed k ≤ v ∧ v - MeasureTheory.SimpleFunc.ennrealRatEmbed k < ε

Density of the rational encoding ennrealRatEmbed in compact intervals [0, C] ⊂ ℝ≥0∞: for any C < ∞ and ε > 0, finitely many rational embeddings (indexed by indices < N) form an ε-net from below for every v ≤ C. This is the discretisation used in the construction of simple-function approximations to measurable functions.