LiftPred — Mathlib

English

Let p be a predicate on β and f be an equivalence class of μ-measurable functions α → β. Then the statement LiftPred(p, f) expresses that p holds for the value f(a) for almost every a ∈ α.

Русский

Пусть p — предикат на β, а f — эквивалентность по μ-модулю для функций α → β. Тогда LiftPred(p, f) означает, что p выполняется для значения f(a) почти для всех a ∈ α.

LaTeX

$$$\operatorname{LiftPred}(p, f) \;\Longleftrightarrow\; \forall^{\mathrm{ae}} a \;\partial\mu,\; p\bigl(f(a)\bigr).$$$

Lean4

/-- Given a predicate `p` and an equivalence class `[f]`, return true if `p` holds of `f a`
for almost all `a` -/
def LiftPred (p : β → Prop) (f : α →ₘ[μ] β) : Prop :=
  f.toGerm.LiftPred p

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