div — Mathlib

English

If the uncurry of f is strongly measurable, then for every x, the function x ↦ f(x) is strongly measurable.

Русский

Если uncurry f сильно измерима, то для каждого x функция f(x) сильно измерима.

LaTeX

$$$\text{StronglyMeasurable}(\text{uncurry } f) \Rightarrow \forall x,\ \text{StronglyMeasurable}(f(x))$$$

Lean4

@[to_additive (attr := fun_prop, aesop safe 20 apply (rule_sets := [Measurable]))]
protected theorem div [Div β] [ContinuousDiv β] (hf : StronglyMeasurable f) (hg : StronglyMeasurable g) :
    StronglyMeasurable (f / g) :=
  ⟨fun n => hf.approx n / hg.approx n, fun x => (hf.tendsto_approx x).div' (hg.tendsto_approx x)⟩

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