English
Adding a trivial unit component to the left argument does not change the StieltjesOfMeasurableRat value: stieltjesOfMeasurableRat (fun (p : Unit × α) => f p.2) (hf.comp measurable_snd) ((), a) = stieltjesOfMeasurableRat f hf a.
Русский
Добавление единичного компонента слева не влияет на значение функции Стильтьджеса: stieltjesOfMeasurableRat (функция, вводящая единицу) ... = stieltjesOfMeasurableRat f hf a.
LaTeX
$$$\text{stieltjesOfMeasurableRat} (\lambda p. f\,p.snd) (hf \circ \text{measurable_snd}) ((), a) = \text{stieltjesOfMeasurableRat} f hf a$$$
Lean4
theorem stieltjesOfMeasurableRat_unit_prod (hf : Measurable f) (a : α) :
stieltjesOfMeasurableRat (fun (p : Unit × α) ↦ f p.2) (hf.comp measurable_snd) ((), a) =
stieltjesOfMeasurableRat f hf a :=
by
simp_rw [stieltjesOfMeasurableRat, IsMeasurableRatCDF.stieltjesFunction, ←
IsMeasurableRatCDF.stieltjesFunctionAux_unit_prod a]
congr 1 with x
congr 1 with p : 1
cases p with
| mk _ b => rw [← toRatCDF_unit_prod b]
