id_comp — Mathlib

English

For a measure μ and kernel κ, the identity map composition leaves μ unchanged: id ∘ₘ μ = μ, and similarly for Markov kernels via equivalences.

Русский

Идентичное отображение не меняет меру: id ∘ₘ μ = μ, аналогично через марковские ядра.

LaTeX

$$$ \text{Kernel.id} \circ_K \kappa = \kappa $$$

Lean4

@[simp]
theorem id_comp : Kernel.id ∘ₘ μ = μ := by rw [Kernel.id, deterministic_comp_eq_map, Measure.map_id]

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