extend_comp_eq' — Mathlib

English

The extension satisfies (f₁.extend g hg f₂) ∘ g = f₁ as functions.

Русский

Расширение удовлетворяет (f₁.extend g hg f₂) ∘ g = f₁ как функция.

LaTeX

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

Lean4

@[simp]
theorem extend_comp_eq' [MeasurableSpace β] (f₁ : α →ₛ γ) {g : α → β} (hg : MeasurableEmbedding g) (f₂ : β →ₛ γ) :
    f₁.extend g hg f₂ ∘ g = f₁ :=
  funext fun _ => extend_apply _ _ _ _

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