English
Let f₁ be a simple function α → γ, g: α → β be measurable embedding, f₂: β →ₛ γ be a simple function. Then (f₁.extend g hg f₂)(g x) = f₁ x for all x.
Русский
Пусть f₁ — простая функция α → γ, g: α → β — встраивание измеримое, f₂ — простая β → γ. Тогда (f₁.extend g hg f₂)(g x) = f₁ x при любых x.
LaTeX
$$$$ (f_1.\\text{extend } g\\; hg\\; f_2)(g\\,x) = f_1\\,x. $$$$
Lean4
@[simp]
theorem extend_apply [MeasurableSpace β] (f₁ : α →ₛ γ) {g : α → β} (hg : MeasurableEmbedding g) (f₂ : β →ₛ γ) (x : α) :
(f₁.extend g hg f₂) (g x) = f₁ x :=
hg.injective.extend_apply _ _ _