diff — Mathlib

English

Difference of two BaireMeasurableSet is BaireMeasurableSet.

Русский

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

LaTeX

$$$$ \mathrm{BaireMeasurableSet}(s) \land \mathrm{BaireMeasurableSet}(t) \Rightarrow \mathrm{BaireMeasurableSet}(s \setminus t). $$$$

Lean4

theorem diff (hs : BaireMeasurableSet s) (ht : BaireMeasurableSet t) : BaireMeasurableSet (s \ t) :=
  MeasurableSet.diff hs ht

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