div — Mathlib

English

If f and g are AEStronglyMeasurable with respect to μ and the target is a topological group, then the quotient f/g is AEStronglyMeasurable.

Русский

Если f и g являются AEStronglyMeasurable относительно μ и целевое пространство является топологической группой, то частное f/g AEStronglyMeasurable.

LaTeX

$$$AEStronglyMeasurable\ f\ μ \rightarrow AEStronglyMeasurable\ g\ μ \rightarrow AEStronglyMeasurable\left( x \mapsto f(x) / g(x) \right) μ$$$

Lean4

@[to_additive (attr := fun_prop, aesop safe 20 apply (rule_sets := [Measurable]))]
protected theorem div [Group β] [IsTopologicalGroup β] (hf : AEStronglyMeasurable[m] f μ)
    (hg : AEStronglyMeasurable[m] g μ) : AEStronglyMeasurable[m] (f / g) μ :=
  ⟨hf.mk f / hg.mk g, hf.stronglyMeasurable_mk.div hg.stronglyMeasurable_mk, hf.ae_eq_mk.div hg.ae_eq_mk⟩

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