LeanMachineLearning exposition

MeasureTheory.Measurable.toNat🔗

Minimal Lean file

toNat🔗

LemmaMeasureTheory.Measurable.toNat
Details

No docstring.

🔗theorem
MeasureTheory.Measurable.toNat.{u_1} {α : Type u_1}
  {mα : MeasurableSpace α} {f : α → ℕ∞} (hf : Measurable f) :
  Measurable fun a => ENat.toNat (f a)
MeasureTheory.Measurable.toNat.{u_1}
  {α : Type u_1} {mα : MeasurableSpace α}
  {f : α → ℕ∞} (hf : Measurable f) :
  Measurable fun a => ENat.toNat (f a)

Code

lemma Measurable.toNat {f : α → ℕ∞} (hf : Measurable f) : Measurable (fun a ↦ (f a).toNat)
Used by (1)

Actions: Source · Open Issue

Proof
Measurable.comp (by fun_prop) hf