EventuallyMeasurableSet — Mathlib

English

A set s is eventually measurable with respect to m and l if s is measurable in the eventuallyMeasurableSpace defined by m and l.

Русский

Множество s является в некотором смысле измеримым относительно m и l, если оно измеримо в пространства eventuallyMeasurableSpace(m,l).

LaTeX

$$$\text{EventuallyMeasurableSet}(m,l,s) \iff s \in \mathrm{MeasurableSet}(\text{eventuallyMeasurableSpace } m l).$$$

Lean4

/-- We say a set `s` is an `EventuallyMeasurableSet` with respect to a given
σ-algebra `m` and σ-filter `l` if it differs from a set in `m` by a set in
the dual ideal of `l`. -/
def EventuallyMeasurableSet (l : Filter α) [CountableInterFilter l] (s : Set α) : Prop :=
  @MeasurableSet _ (eventuallyMeasurableSpace m l) s

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