extend_apply' — Mathlib

English

If there is no x with g x = y, then (f₁.extend g hg f₂) y = f₂ y.

Русский

Если не существует x such that g x = y, тогда (f₁.extend g hg f₂) y = f₂ y.

LaTeX

$$$$ \\neg \\exists x\\, (g x = y) \\Rightarrow (f_1.\\text{extend } g\\; hg\\; f_2)\\, y = f_2\\, y. $$$$

Lean4

@[simp]
theorem extend_apply' [MeasurableSpace β] (f₁ : α →ₛ γ) {g : α → β} (hg : MeasurableEmbedding g) (f₂ : β →ₛ γ) {y : β}
    (h : ¬∃ x, g x = y) : (f₁.extend g hg f₂) y = f₂ y :=
  Function.extend_apply' _ _ _ h

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