fst_real_apply — Mathlib

English

In real-valued measure terms, (fst κ a).real S equals (κ a).real {p | p.1 ∈ S} for measurable S.

Русский

В терминах вещественных мер: (fst κ a).real S = (κ a).real {p | p.1 ∈ S} для измеримого S.

LaTeX

$$$$ (fst \\kappa a).real S = (\\kappa a).real \\{ p \\mid p.1 \\in S \\} $$$$

Lean4

theorem fst_real_apply (κ : Kernel α (β × γ)) (a : α) {s : Set β} (hs : MeasurableSet s) :
    (fst κ a).real s = (κ a).real {p | p.1 ∈ s} := by simp [fst_apply', hs, measureReal_def]

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