English
A function is EventuallyMeasurable if the preimage of any measurable set is equal, modulo l, to some m-measurable set.
Русский
Функция является EventuallyMeasurable если для любого измеримого множества его прообраз равен по модулю l некоторому множества, измеримому относительно m.
LaTeX
$$$f: α \to β \quad \Rightarrow\quad \forall S,\ MeasurableSet_m(S) \Rightarrow f^{-1}(S) =_l T \text{ для некоторого } T \in m.$$$
Lean4
/-- We say a function is `EventuallyMeasurable` with respect to a given
σ-algebra `m` and σ-filter `l` if the preimage of any measurable set is equal to some
`m`-measurable set modulo `l`.
Warning: This is not always the same as being equal to some `m`-measurable function modulo `l`.
In general it is weaker. See `Measurable.eventuallyMeasurable_of_eventuallyEq`.
*TODO*: Add lemmas about when these are equivalent. -/
def EventuallyMeasurable (f : α → β) : Prop :=
@Measurable _ _ (eventuallyMeasurableSpace m l) _ f
