map_apply — Mathlib

English

For measurable f, map_apply κ f a equals (κ a).map f; map_apply' extends this to measurable sets.

Русский

При измеримости f имеем map_apply κ f a = (κ a).map f; map_apply' расширяет это на измеримые множества.

LaTeX

$$$$\\text{map_apply}(κ,f,a) = (κ a).map f.$$$$

Lean4

theorem map_apply (κ : Kernel α β) (hf : Measurable f) (a : α) : map κ f a = (κ a).map f := by
  simp only [map, hf, ↓reduceDIte, mapOfMeasurable, coe_mk]

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