diff — Mathlib

English

The difference of two null measurable sets is null measurable.

Русский

Разность двух нулевых измеримых множеств остаётся нулевой измеримой.

LaTeX

$$$\\text{NullMeasurableSet } s μ \\land \\text{NullMeasurableSet } t μ \\Rightarrow \\text{NullMeasurableSet } (s \\setminus t) μ$$$

Lean4

@[simp]
protected theorem diff (hs : NullMeasurableSet s μ) (ht : NullMeasurableSet t μ) : NullMeasurableSet (s \ t) μ :=
  MeasurableSet.diff hs ht

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