nullMeasurableSet_mulSupport — Mathlib

English

If f and g are AEStronglyMeasurable, then the set {a | f(a) < g(a)} is null-measurable.

Русский

Если f и g — AEStronglyMeasurable, множество {a | f(a) < g(a)} нуль-измеримо.

LaTeX

$$$AEStronglyMeasurable(f, \mu) \land AEStronglyMeasurable(g, \mu) \Rightarrow NullMeasurableSet\{a \mid f(a) < g(a)\}, \mu$$$

Lean4

@[to_additive]
theorem nullMeasurableSet_mulSupport {E} [TopologicalSpace E] [MetrizableSpace E] [One E] {f : α → E}
    (hf : AEStronglyMeasurable f μ) : NullMeasurableSet (mulSupport f) μ :=
  (hf.nullMeasurableSet_eq_fun stronglyMeasurable_const.aestronglyMeasurable).compl

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