LeanMachineLearning exposition

MeasureTheory.Measurable.coe_nat_enat🔗

Minimal Lean file

coe_nat_enat🔗

LemmaMeasureTheory.Measurable.coe_nat_enat
Details

No docstring.

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

Code

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

Actions: Source · Open Issue

Proof
Measurable.comp (by fun_prop) hf