approx — Mathlib

English

If f and g are Finite Strongly Measurable, then their pointwise sum f+g is Finite Strongly Measurable.

Русский

Если f и g финально сильно измеримы, то их сумма f+g тоже финально сильно измерима.

LaTeX

$$$\text{FinStronglyMeasurable}(f)\mu \wedge \text{FinStronglyMeasurable}(g)\mu \Rightarrow \text{FinStronglyMeasurable}(f+g)\mu$$$

Lean4

/-- A sequence of simple functions such that `∀ x, Tendsto (fun n ↦ hf.approx n x) atTop (𝓝 (f x))`
and `∀ n, μ (support (hf.approx n)) < ∞`. These properties are given by
`FinStronglyMeasurable.tendsto_approx` and `FinStronglyMeasurable.fin_support_approx`. -/
protected noncomputable def approx : ℕ → α →ₛ β :=
  hf.choose

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