extend_apply — Mathlib

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 _ _ _

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