inter — Mathlib

English

Intersection of two BaireMeasurableSet is BaireMeasurableSet.

Русский

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

LaTeX

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

Lean4

theorem inter (hs : BaireMeasurableSet s) (ht : BaireMeasurableSet t) : BaireMeasurableSet (s ∩ t) :=
  MeasurableSet.inter hs ht

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