coe_nnreal_ennreal — Mathlib

English

IdentDistrib is preserved under the natural-embedding from NNReal to ENNReal.

Русский

Сохранение распределения при естественном вложении NNReal в ENNReal.

LaTeX

$$$\text{IdentDistrib} f g\ \mu\ nu \Rightarrow \text{IdentDistrib} (\lambda x. (f x : \mathbb{R}_{\ge 0}^{}) ) (\lambda x. (g x : \mathbb{R}_{\ge 0}^{}) )\ mu\ nu$$$

Lean4

protected theorem coe_nnreal_ennreal {f : α → ℝ≥0} {g : β → ℝ≥0} (h : IdentDistrib f g μ ν) :
    IdentDistrib (fun x => (f x : ℝ≥0∞)) (fun x => (g x : ℝ≥0∞)) μ ν :=
  h.comp measurable_coe_nnreal_ennreal

Похожие утверждения