div — Mathlib

English

If f and g are measurable, then x ↦ f(x) / g(x) is measurable.

Русский

Если f и g измеримы, то x ↦ f(x) / g(x) измеримо.

LaTeX

$$$\\text{Measurable}(f) \\land \\text{Measurable}(g) \\Rightarrow \\text{Measurable}(x \\mapsto f(x) / g(x)).$$$

Lean4

@[to_additive (attr := fun_prop, aesop safe 20 apply (rule_sets := [Measurable]))]
theorem div [MeasurableDiv₂ G] (hf : Measurable f) (hg : Measurable g) : Measurable fun a => f a / g a :=
  measurable_div.comp (hf.prodMk hg)

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