eventuallyMeasurableSet — Mathlib

English

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

Русский

Если s измеримо относительно m, то оно в смысле «в итоге» измеримо относительно m и l.

LaTeX

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

Lean4

theorem eventuallyMeasurableSet (hs : MeasurableSet s) : EventuallyMeasurableSet m l s :=
  ⟨s, hs, EventuallyEq.refl _ _⟩

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