div' — Mathlib

English

If hf : Measurable ↿f, hg : Measurable ↿g, and hh : Measurable h, then a ↦ (f(a)/g(a))(h(a)) is measurable.

Русский

Если f и g — измеримые и h — измеримая, то a ↦ (f(a)/g(a))(h(a)) измеримо.

LaTeX

$$$\\text{Measurable}(f) \\Rightarrow \\text{Measurable}(g) \\Rightarrow \\text{Measurable}(a \\mapsto (f(a)/g(a))(h(a))).$$$

Lean4

@[to_additive (attr := fun_prop, aesop safe 20 apply (rule_sets := [Measurable]))]
theorem div' [MeasurableDiv₂ G] {f g : α → β → G} {h : α → β} (hf : Measurable ↿f) (hg : Measurable ↿g)
    (hh : Measurable h) : Measurable fun a ↦ (f a / g a) (h a) := by dsimp; fun_prop

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