fst_apply' — Mathlib

English

For a κ, a and a measurable set s ⊆ β, fst κ a (s) = κ a { p | p.1 ∈ s }.

Русский

Для κ, a и измеримого множества s ⊆ β: fst κ a (s) = κ a { p | p.1 ∈ s }.

LaTeX

$$$$fst \\kappa a \\; S = \\kappa a \\{ p \\mid p.1 \\in S \\}$$$$

Lean4

theorem fst_apply' (κ : Kernel α (β × γ)) (a : α) {s : Set β} (hs : MeasurableSet s) : fst κ a s = κ a {p | p.1 ∈ s} :=
  by rw [fst_apply, Measure.map_apply measurable_fst hs]; rfl

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