extend_comp_eq — Mathlib

English

The extended function composed with g (with measurability) equals f₁.

Русский

Расширенная функция в составе с g (при измеримости) равна f₁.

LaTeX

$$$$ (f_1.\\text{extend } g\\; hg\\; f_2).\\text{comp } g\\; hg.\\text{measurable} = f_1. $$$$

Lean4

@[simp]
theorem extend_comp_eq [MeasurableSpace β] (f₁ : α →ₛ γ) {g : α → β} (hg : MeasurableEmbedding g) (f₂ : β →ₛ γ) :
    (f₁.extend g hg f₂).comp g hg.measurable = f₁ :=
  coe_injective <| extend_comp_eq' _ hg _

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