English
Given a relation r on β and γ, and two μ-a.e.-equivalence classes f ∈ α →ₘ[μ] β and g ∈ α →ₘ[μ] γ, LiftRel(r, f, g) holds exactly when r holds between f(a) and g(a) for almost every a ∈ α.
Русский
Для отношения r между β и γ и двух классов эквивалентности по μ почти везде f ∈ α →ₘ[μ] β и g ∈ α →ₘ[μ] γ, выполняется LiftRel(r, f, g) тогда и только тогда, когда для почти всех a ∈ α выполняется r(f(a), g(a)).
LaTeX
$$$\operatorname{LiftRel}(r, f, g) \;\Longleftrightarrow\; \forall^{\mathrm{ae}} a \;\partial\mu,\; r\bigl(f(a), g(a)\bigr).$$$
Lean4
/-- Given a relation `r` and equivalence class `[f]` and `[g]`, return true if `r` holds of
`(f a, g a)` for almost all `a` -/
def LiftRel (r : β → γ → Prop) (f : α →ₘ[μ] β) (g : α →ₘ[μ] γ) : Prop :=
f.toGerm.LiftRel r g.toGerm
