snd

Mathlib.MeasureTheory.MeasurableSpace.Constructions

URI: https://scilib.ai/kg/mathlib#Measurable.snd

English

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

Русский

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

LaTeX

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

Lean4

@[fun_prop]
theorem snd {f : α → β × γ} (hf : Measurable f) : Measurable fun a : α => (f a).2 :=
  measurable_snd.comp hf

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

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

Разделы

Аффилиация

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