eventuallyMeasurableSet_of_mem_filter

Mathlib.MeasureTheory.MeasurableSpace.EventuallyMeasurable

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

English

If s ∈ l, then s is eventually measurable with respect to m and l.

Русский

Если s принадлежит фильтру l, то s является в итоге измеримым по отношению к m и l.

LaTeX

$$$s \in l \Rightarrow \text{EventuallyMeasurableSet}(m,l,s).$$$

Lean4

theorem eventuallyMeasurableSet_of_mem_filter (hs : s ∈ l) : EventuallyMeasurableSet m l s :=
  ⟨univ, MeasurableSet.univ, eventuallyEq_univ.mpr hs⟩

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

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

Разделы

Аффилиация

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