measurable_prodMk_left

Mathlib.MeasureTheory.MeasurableSpace.Constructions

URI: https://scilib.ai/kg/mathlib#measurable_prodMk_left

English

If x is not in the atom of y, then the atoms are disjoint.

Русский

Если x не принадлежит атомy y, то атомы x и y не пересекаются.

LaTeX

$$$$ x \notin \operatorname{measurableAtom}(y) \Rightarrow \operatorname{measurableAtom}(x) \cap \operatorname{measurableAtom}(y) = \emptyset $$$$

Lean4

theorem measurable_prodMk_left {x : α} : Measurable (@Prod.mk _ β x) :=
  measurable_const.prodMk measurable_id

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru