restrict_univ — Mathlib

English

Let κ be a kernel κ: α → β. Restricting κ to the universal measurable set leaves κ unchanged; i.e., restricting κ to univ is the same kernel.

Русский

Пусть κ — ядро κ: α → β. Ограничение κ до всеобъемлющего множества множества измеримых множеств возвращает то же самое ядро.

LaTeX

$$$\\kappa|_{\\text{univ}} = \\kappa$$$

Lean4

@[simp]
theorem restrict_univ : κ.restrict MeasurableSet.univ = κ :=
  by
  ext1 a
  rw [Kernel.restrict_apply, Measure.restrict_univ]

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